Lines Matching refs:IDENT
72 | Absyn.IDENT (locn,i) =>
105 fun col set l s = (Redblackset.add (set,s), Absyn.IDENT (l, s))
130 (qv', Absyn.IDENT (l, i'))
131 end else (qv, Absyn.IDENT (l, i))
154 (set, Absyn.mk_AQ (assoc i substL))) handle HOL_ERR _ => (set, Absyn.IDENT (l, i))
168 | Absyn.IDENT (locn,i) => (os_opt, l)
170 | Absyn.APP (locn,Absyn.IDENT(_,"old"),Absyn.IDENT(_,v)) =>
183 (SOME os', Absyn.IDENT (locn,(fst o dest_var) nv))
223 (set, Absyn.IDENT (l, i'))
897 Absyn.list_mk_app (Absyn.IDENT (locn.Loc_None, "asl_comment_loop_invariant"), [
901 Absyn.list_mk_app (Absyn.IDENT (locn.Loc_None, "asl_comment_loop_unroll"), [
940 Absyn.IDENT (locn.Loc_None, if loop then "asl_comment_loop_spec" else
944 Absyn.list_mk_app (Absyn.IDENT (locn.Loc_None, "asl_comment_loop_unroll"), [
979 Absyn.IDENT (locn.Loc_None, "asl_comment_assert"), abs_p_a);