diff options
| author | ppedrot | 2013-03-19 15:18:03 +0000 |
|---|---|---|
| committer | ppedrot | 2013-03-19 15:18:03 +0000 |
| commit | 508e8afd8538dd38afa4eaa0dd9c7e349e50e20d (patch) | |
| tree | a1b2f16de9eb4f35f49f6bf598331a7518588a7f /interp | |
| parent | 906b063b798e6c0787fd8f514b9d7f1f8eef9cf8 (diff) | |
Removing the module Libtypes and unifying the Search[Pattern|Rewrite]?
mechanism with the SearchAbout one. Searches may be slower, but this
is unlikely to be noticed. In addition, according to Hugo, the
Libtype summary was imposing a noticeable time penalty without
any real advantage.
Now Search and SearchPattern are the same. The documentation was not
really clear about the difference between both, except that Search
was restricted to closed terms. This is an artificial restriction by
now.
Fixing #2815 btw.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16320 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index a677eb93ed..1d25bc1d9c 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1685,15 +1685,15 @@ let interp_open_constr sigma env c = let interp_open_constr_patvar sigma env c = let raw = intern_gen (OfType None) sigma env c ~allow_patvar:true in let sigma = ref sigma in - let evars = ref (Gmap.empty : (Id.t,glob_constr) Gmap.t) in + let evars = ref (Id.Map.empty : glob_constr Id.Map.t) in let rec patvar_to_evar r = match r with | GPatVar (loc,(_,id)) -> - ( try Gmap.find id !evars + ( try Id.Map.find id !evars with Not_found -> let ev = Evarutil.e_new_evar sigma env (Termops.new_Type()) in let ev = Evarutil.e_new_evar sigma env ev in let rev = GEvar (loc,(fst (Term.destEvar ev)),None) (*TODO*) in - evars := Gmap.add id rev !evars; + evars := Id.Map.add id rev !evars; rev ) | _ -> map_glob_constr patvar_to_evar r in |