diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-10 20:54:19 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-10 20:54:19 +0000 |
| commit | 318c4ba9825b32e41d354473496926f081ea1a52 (patch) | |
| tree | e46ed05c47c1d482711634ad4119c1215796b86c | |
| parent | 1ff9becb45683f9377e1e6337d26f95d976b3ce9 (diff) | |
Removing Gmap from Tacinterp.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16507 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/tacintern.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 9ae7775ca..6a1a33fb0 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -156,10 +156,10 @@ let lookup_tactic s = (* Summary and Object declaration *) let mactab = - Summary.ref (Gmap.empty : (ltac_constant,glob_tactic_expr) Gmap.t) + Summary.ref (KNmap.empty : glob_tactic_expr KNmap.t) ~name:"tactic-definition" -let lookup_ltacref r = Gmap.find r !mactab +let lookup_ltacref r = KNmap.find r !mactab (* We have identifier <| global_reference <| constr *) @@ -858,8 +858,8 @@ let glob_tactic_env l env x = (* Tactic registration *) (* Declaration of the TAC-DEFINITION object *) -let add (kn,td) = mactab := Gmap.add kn td !mactab -let replace (kn,td) = mactab := Gmap.add kn td (Gmap.remove kn !mactab) +let add (kn,td) = mactab := KNmap.add kn td !mactab +let replace (kn,td) = mactab := KNmap.add kn td (KNmap.remove kn !mactab) type tacdef_kind = | NewTac of Id.t @@ -943,7 +943,7 @@ let make_absolute_name ident repl = else let id = coerce_reference_to_id ident in Some id, Lib.make_kn id in - if Gmap.mem kn !mactab then + if KNmap.mem kn !mactab then if repl then id, kn else user_err_loc (loc,"Tacinterp.add_tacdef", |