From 508e8afd8538dd38afa4eaa0dd9c7e349e50e20d Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 19 Mar 2013 15:18:03 +0000
Subject: 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
---
 interp/constrintern.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'interp/constrintern.ml')

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
-- 
cgit v1.2.3