diff options
Diffstat (limited to 'tactics/tacintern.ml')
| -rw-r--r-- | tactics/tacintern.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 9a8774b11..0f2ac6cfe 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -53,9 +53,9 @@ let skip_metaid = function (** Generic arguments *) type glob_sign = { - ltacvars : identifier list * identifier list; + ltacvars : Id.t list * Id.t list; (* ltac variables and the subset of vars introduced by Intro/Let/... *) - ltacrecvars : (identifier * ltac_constant) list; + ltacrecvars : (Id.t * ltac_constant) list; (* ltac recursive names *) gsigma : Evd.evar_map; genv : Environ.env } @@ -87,10 +87,10 @@ let lookup_intern_genarg id = (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) -let atomic_mactab = ref Idmap.empty +let atomic_mactab = ref Id.Map.empty let add_primitive_tactic s tac = - let id = id_of_string s in - atomic_mactab := Idmap.add id tac !atomic_mactab + let id = Id.of_string s in + atomic_mactab := Id.Map.add id tac !atomic_mactab let _ = let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in @@ -124,10 +124,10 @@ let _ = "fresh", TacArg(dloc,TacFreshId []) ] -let lookup_atomic id = Idmap.find id !atomic_mactab +let lookup_atomic id = Id.Map.find id !atomic_mactab let is_atomic_kn kn = let (_,_,l) = repr_kn kn in - Idmap.mem (id_of_label l) !atomic_mactab + Id.Map.mem (id_of_label l) !atomic_mactab (* Tactics table (TacExtend). *) @@ -753,7 +753,7 @@ and intern_tacarg strict onlytac ist = function | ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c) | MetaIdArg (loc,istac,s) -> (* $id can occur in Grammar tactic... *) - let id = id_of_string s in + let id = Id.of_string s in if find_ltacvar id ist then if istac then Reference (ArgVar (adjust_loc loc,id)) else ConstrMayEval (ConstrTerm (GVar (adjust_loc loc,id), None)) @@ -865,7 +865,7 @@ let add (kn,td) = mactab := Gmap.add kn td !mactab let replace (kn,td) = mactab := Gmap.add kn td (Gmap.remove kn !mactab) type tacdef_kind = - | NewTac of identifier + | NewTac of Id.t | UpdateTac of ltac_constant let load_md i ((sp,kn),(local,defs)) = |