=?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=20[whd=5Fevar]=20:=20les

=20evar=5Fdefs=20gardent=20un=20cache=20des=20appels=20pr=C3=A9c=C3=A9dents.=20Le=20d=C3=A9faut=20de=20la
=20m=C3=A9thodologie=20est=20que=20=C3=A7a=20int=C3=A9ragit=20assez=20mal=20avec=20la=20substitution=20des
=20hypoth=C3=A8ses=20de=20l'evar=20(qui=20n'est=20pas=20mise=20en=20cache).=20En=20particulier=20les
=20deux=20fonctions=20ne=20sont=20plus=20r=C3=A9cursives=20terminales.=20De=20plus=20un=20appel=20=C3=A0
=20l'une=20des=20deux=20fera=20n=C3=A9cessairement=20un=20parcours=20du=20terme=20pour=20appliquer
=20la=20substitution.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit

D'un point de vue de l'effet observer, ça a un effet assez léger sur le
trunk, je suis curieux de voir les effets sur les contribs.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11950 85f007b7-540e-0410-9357-904b9bb8a0f7

12 files changed, 180 insertions, 55 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 75b811d518..dbe11a4370 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -200,7 +200,7 @@ let isAppConstruct ?(env=Global.env ()) t =
 
 let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta  *)
   let clos_norm_flags flgs env sigma t =
-    Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
+    Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Evd.nf_evar sigma t)) in
   clos_norm_flags Closure.betaiotazeta  Environ.empty_env Evd.empty
     
 
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index 69cc0607b6..2c930ac033 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -197,12 +197,12 @@ let extract_pftreestate pts =
 
 let nf_betaiotazeta =
   let clos_norm_flags flgs env sigma t =
-    Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
+    Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Evd.nf_evar sigma t)) in
   clos_norm_flags Closure.betaiotazeta  
 
 let nf_betaiota =
   let clos_norm_flags flgs env sigma t =
-    Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
+    Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Evd.nf_evar sigma t)) in
   clos_norm_flags Closure.betaiota  
 
 let cook_proof do_reduce =
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 29b5b87a7d..d0ed4f1363 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -58,10 +58,10 @@ let jv_nf_evar = Pretype_errors.jv_nf_evar
 let tj_nf_evar = Pretype_errors.tj_nf_evar
 
 let nf_named_context_evar sigma ctx = 
-  Sign.map_named_context (Reductionops.nf_evar sigma) ctx
+  Sign.map_named_context (Evd.nf_evar sigma) ctx
 
 let nf_rel_context_evar sigma ctx = 
-  Sign.map_rel_context (Reductionops.nf_evar sigma) ctx
+  Sign.map_rel_context (Evd.nf_evar sigma) ctx
     
 let nf_env_evar sigma env = 
   let nc' = nf_named_context_evar sigma (Environ.named_context env) in
@@ -70,11 +70,11 @@ let nf_env_evar sigma env =
 
 let nf_evar_info evc info =
   { info with 
-    evar_concl = Reductionops.nf_evar evc info.evar_concl;
-    evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps;
+    evar_concl = Evd.nf_evar evc info.evar_concl;
+    evar_hyps = map_named_val (Evd.nf_evar evc) info.evar_hyps;
     evar_body = match info.evar_body with
       | Evar_empty -> Evar_empty
-      | Evar_defined c -> Evar_defined (Reductionops.nf_evar evc c) }
+      | Evar_defined c -> Evar_defined (Evd.nf_evar evc c) }
 
 let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi))
 		     evm Evd.empty
@@ -112,7 +112,7 @@ let push_dependent_evars sigma emap =
   Evd.fold (fun ev {evar_concl = ccl} (sigma',emap') ->
     List.fold_left 
       (fun (sigma',emap') ev -> 
-	(Evd.add sigma' ev (Evd.find emap' ev),Evd.remove emap' ev))
+	(Evd.add sigma' ev (Evd.find emap' ev),Evd.unsafe_remove emap' ev))
       (sigma',emap') (collect_evars emap' ccl))
     emap (sigma,emap)
 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 6bc77abcb6..a5d36f9141 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -65,9 +65,9 @@ let eq_evar_info ei1 ei2 =
 
 (* spiwack: Revised hierarchy :
       - ExistentialMap ( Maps of existential_keys )
-      - EvarInfoMap ( .t = evar_info ExistentialMap.t )
+      - EvarInfoMap ( .t ~ evar_info ExistentialMap.t )
       - EvarMap ( .t = EvarInfoMap.t * sort_constraints )
-      - evar_defs (exported)
+      - evar_defs (= unification states, exported)
 *)
 
 module ExistentialMap = Intmap
@@ -77,24 +77,65 @@ module ExistentialSet = Intset
 exception NotInstantiatedEvar
 
 module EvarInfoMap = struct
-  type t = evar_info ExistentialMap.t
-
-  let empty = ExistentialMap.empty
-
-  let to_list evc = (* Workaround for change in Map.fold behavior *)
+   (**************************************************************
+    * EvarInfoMap represents maps from [evar] to [evar_info] (that is
+    * a structure which associates to existential variables their type
+    * and possibly their definition (aka body)) plus certain cached
+    * information (values of [whd_evar] and [nf_evar] on those 
+    * existential variables before substituting anything for their 
+    * hypotheses).
+    * Caches are represented as mutable cells (in the type 
+    * [cached_info] which encapsulates [evar_info]) to keep caching 
+    * transparent to the interface. The down side of using mutable 
+    * cells in a persistant data-structure is that mutations influence
+    * past versions of the structure. To ensure that the structure stays
+    * pure we have to  track a "version number" together with the 
+    * cache. If the cache is more recent than the structure then it is
+    * considered inconsistent and discarded.
+    * The price is that we cannot say much about the effect of 
+    * caching in the worst case. Also caching makes [nf_evar]
+    * and [whd_evar] non-tail recursive (because substitution of
+    * the hypotheses is delayed). Which may make them inefficient
+    * in some cases.
+    *************************************************************)
+
+
+  (* Invariant: whd and nf are [None] while evar_info.evar_body is [Evar_Empty] *)
+  type cached_info = { 
+      evar_info : evar_info ;
+      (* stores the last computed whd of the existential variale. *)
+      mutable whd : (int*constr) option;
+      (* stores the last computed nf (=fully instantiated value) of the existential var.*)
+      mutable nf : (int*constr) option
+  } 
+  let empty_cache ei = { evar_info=ei;whd=None;nf=None }
+
+  (* mapping * version number *)
+  type t = cached_info ExistentialMap.t*int
+
+  let empty = (ExistentialMap.empty,0)
+
+  let to_list (evc,_) = (* Workaround for change in Map.fold behavior *)
     let l = ref [] in 
-    ExistentialMap.iter (fun evk x -> l := (evk,x)::!l) evc;
+    ExistentialMap.iter (fun evk x -> l := (evk,x.evar_info)::!l) evc;
     !l
 
-  let dom evc = ExistentialMap.fold (fun evk _ acc -> evk::acc) evc []
-  let find evc k = ExistentialMap.find k evc
-  let remove evc k = ExistentialMap.remove k evc
-  let mem evc k = ExistentialMap.mem k evc
-  let fold = ExistentialMap.fold
+  let dom (evc,_) = ExistentialMap.fold (fun evk _ acc -> evk::acc) evc []
+  let find (evc,_) k = (ExistentialMap.find k evc).evar_info
+  let mem (evc,_) k = ExistentialMap.mem k evc
+
+  let add (evd,v) evk newinfo =  
+    (ExistentialMap.add evk (empty_cache newinfo) evd,v+1)
 
-  let add evd evk newinfo =  ExistentialMap.add evk newinfo evd
+  (* spiwack: this should be considered deprecated *)
+  let unsafe_remove (evc,v) k = (ExistentialMap.remove k evc,v+1)
 
-  let equal = ExistentialMap.equal
+  let map f (evc,v)= 
+    (ExistentialMap.map (fun ci -> empty_cache (f ci.evar_info)) evc,0)
+  let fold f (evc,_)= ExistentialMap.fold (fun evk ci acc -> f evk ci.evar_info acc) evc
+
+  let equal f (evc1,_) (evc2,_) = 
+    ExistentialMap.equal (fun ci1 ci2 -> f ci1.evar_info ci2.evar_info) evc1 evc2
 
   let define evd evk body = 
     let oldinfo =
@@ -104,7 +145,7 @@ module EvarInfoMap = struct
       { oldinfo with
 	  evar_body = Evar_defined body } in
       match oldinfo.evar_body with
-	| Evar_empty -> ExistentialMap.add evk newinfo evd
+	| Evar_empty -> add evd evk newinfo
 	| _ -> anomaly "Evd.define: cannot define an evar twice"
 
   let is_evar sigma evk = mem sigma evk
@@ -151,19 +192,82 @@ module EvarInfoMap = struct
     let hyps = evar_filtered_context info in
       instantiate_evar hyps info.evar_concl (Array.to_list args)
 
+  let get_evar_body evi =
+    match evar_body evi with
+      | Evar_defined c -> c 
+      | Evar_empty -> raise NotInstantiatedEvar
+    
   let existential_value sigma (n,args) =
     let info = find sigma n in
     let hyps = evar_filtered_context info in
-      match evar_body info with
-	| Evar_defined c ->
-	    instantiate_evar hyps c (Array.to_list args)
-	| Evar_empty ->
-	    raise NotInstantiatedEvar
+    let c = get_evar_body info in
+    instantiate_evar hyps c (Array.to_list args)
 
   let existential_opt_value sigma ev =
     try Some (existential_value sigma ev)
     with NotInstantiatedEvar -> None
 
+  (*** Computing instantiated forms of existential variables. ***)
+
+  let get_whd_cache ci = ci.whd
+  let set_whd_cache ci v c = ci.whd <- Some (v,c)
+  let get_nf_cache ci = ci.nf
+  let set_nf_cache ci v c = ci.nf <- Some (v,c)
+
+  (* [inst_gen] is the prototype for [whd_evar] and [nf_evar]. It takes
+      as additional parameters a pair of arguments [set]/[get] which 
+      are meant to respectively cache a ([constr]) value (together with
+      a version number) and return the value previously cached by [set].
+      It also takes an argument [r] which specifies what to do on non-[Evar]
+      terms. That is "just return it" for [whd_evar], and "operate recursively
+      on subterms" for [nf_evar]. *)
+  let rec inst_gen set get r sigma c =
+    match kind_of_term c with
+      | Evar (e,args) -> 
+	  begin try 
+	    let (c',hyps) = inst_gen_of_evar set get r sigma e in
+	    instantiate_evar hyps c' (Array.to_list args)
+	  with Not_found | NotInstantiatedEvar -> c end
+      | _ -> r c
+  and inst_gen_of_evar set get r ((sigma,v) as evc) e =
+    let oci =  ExistentialMap.find e sigma in
+    let info = oci.evar_info in
+    let hyps = evar_filtered_context info in
+    match get oci with
+      | None ->
+	  (* The cache is empty. 
+	      We call [inst_gen] recursively to construct the cache. *)
+	  let c = get_evar_body info in
+	  let c' = inst_gen set get r evc c in
+	  set oci v c';
+	  (c', hyps)
+      | Some (v',_) when v' > v ->
+	  (* This is a copy of previous case. It'd be better to factorise it somehow,
+	      but "when" clauses cannot operate on operands of or-patterns. *)
+	  (* The cache is inconsistent (comes from a future version
+	      of the map). 
+	      We call [inst_gen] recursively to construct the cache. *)
+	  let c = get_evar_body info in
+	  let c' = inst_gen set get r evc c in
+	  set oci v c';
+	  (c', hyps)
+      | Some (v',c) when v' < v -> 
+	  (* The cache is consistent but not necessarily complete. 
+	      It comes from a past version of the map.
+	      We call [inst_gen] recursively on the cached value, 
+	      and update the cache. *)
+	  let c' = inst_gen set get r evc c in
+	  set oci v c';
+	  (c', hyps)
+      | Some (_,c') (*when v'=v *) ->
+	  (* The cache is fully consistent, as it has been made on
+	      this version of the map. We can simply return it. *)
+	  (c', hyps)
+
+  let  whd_evar = inst_gen set_whd_cache get_whd_cache Util.identity
+  let rec nf_evar sigma c = 
+    inst_gen set_nf_cache get_nf_cache (map_constr  (nf_evar sigma)) sigma c
+
 end
 
 (*******************************************************************)
@@ -237,6 +341,11 @@ let is_sort_var s scstr =
         with Not_found -> false)
     | _ -> false
 
+let rec nf_sort_var scstr t =
+  match kind_of_term t with
+    | Sort s when is_sort_var s scstr -> whd_sort_var scstr t
+    | _ -> map_constr (nf_sort_var scstr) t
+
 let new_sort_var cstr =
   let u = Termops.new_univ() in
   (u, UniverseMap.add u (SortVar([],[])) cstr)
@@ -305,7 +414,8 @@ module EvarMap = struct
   let add (sigma,sm) k v = (EvarInfoMap.add sigma k v, sm)
   let dom (sigma,_) = EvarInfoMap.dom sigma
   let find (sigma,_) = EvarInfoMap.find sigma
-  let remove (sigma,sm) k = (EvarInfoMap.remove sigma k, sm)
+  (* spiwack: unsafe_remove should be considered deprecated *)
+  let unsafe_remove (sigma,sm) k = (EvarInfoMap.unsafe_remove sigma k, sm)
   let mem (sigma,_) = EvarInfoMap.mem sigma
   let to_list (sigma,_) = EvarInfoMap.to_list sigma
   let fold f (sigma,_) = EvarInfoMap.fold f sigma
@@ -321,6 +431,17 @@ module EvarMap = struct
 
   let merge e e' = fold (fun n v sigma -> add sigma n v) e' e
   
+  let whd_evar (sigma,sm) c =
+    let c = EvarInfoMap.whd_evar sigma c in
+    match kind_of_term c with
+      | Sort s when is_sort_var s sm -> whd_sort_var sm c
+      | _ -> c
+
+
+  let nf_evar (sigma,sm) c =
+    let c = EvarInfoMap.nf_evar sigma c in
+    nf_sort_var sm c
+
 end
  
 (*******************************************************************)
@@ -446,7 +567,8 @@ let merge d1 d2 = {
   metas = Metamap.fold (fun k m r -> Metamap.add k m r) d2.metas d1.metas
 }
 let add d e i = { d with evars=EvarMap.add d.evars e i }
-let remove d e = { d with evars=EvarMap.remove d.evars e }
+(* spiwack: unsafe_remove should be considered deprecated *)
+let unsafe_remove d e = { d with evars=EvarMap.unsafe_remove d.evars e }
 let dom d = EvarMap.dom d.evars
 let find d e = EvarMap.find d.evars e
 let mem d e = EvarMap.mem d.evars e
@@ -486,7 +608,7 @@ let subst_evar_defs_light sub evd =
   assert (evd.conv_pbs = []);
   { evd with
       metas = Metamap.map (map_clb (subst_mps sub)) evd.metas;
-      evars = ExistentialMap.map (subst_evar_info sub)  (fst evd.evars), snd evd.evars
+      evars = EvarInfoMap.map (subst_evar_info sub)  (fst evd.evars), snd evd.evars
   }
 
 let subst_evar_map = subst_evar_defs_light
@@ -579,6 +701,8 @@ let extract_all_conv_pbs evd =
 let evar_merge evd evars =
   { evd with evars = EvarMap.merge evd.evars evars.evars }
 
+
+
 (**********************************************************)
 (* Sort variables *)
 
@@ -595,6 +719,12 @@ let define_sort_variable ({evars=(sigma,sm)}as d) u s =
 let pr_sort_constraints {evars=(_,sm)} = pr_sort_cstrs sm
 
 (**********************************************************)
+(* Substitution of existential variables  *)
+
+let whd_evar { evars=em } t = EvarMap.whd_evar em t
+let nf_evar { evars=em } t = EvarMap.nf_evar em t
+
+(**********************************************************)
 (* Accessing metas *)
 
 let meta_list evd = metamap_to_list evd.metas
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index ac708d1ec7..da1cfd130e 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -132,7 +132,6 @@ val add : evar_defs -> evar -> evar_info -> evar_defs
 
 val dom : evar_defs -> evar list
 val find : evar_defs -> evar -> evar_info
-val remove : evar_defs -> evar -> evar_defs
 val mem : evar_defs -> evar -> bool
 val to_list : evar_defs -> (evar * evar_info) list
 val fold : (evar -> evar_info -> 'a -> 'a) -> evar_defs -> 'a -> 'a
@@ -240,6 +239,13 @@ val whd_sort_variable : evar_defs -> constr -> constr
 val set_leq_sort_variable : evar_defs -> sorts -> sorts -> evar_defs
 val define_sort_variable : evar_defs -> sorts -> sorts -> evar_defs
 
+
+(**********************************************************)
+(* Substitution of existential variables  *)
+
+val whd_evar : evar_defs -> constr -> constr
+val nf_evar : evar_defs -> constr -> constr
+
 (*********************************************************************)
 (* constr with holes *)
 type open_constr = evar_defs * constr
@@ -275,4 +281,5 @@ val create_evar_defs      : evar_defs -> evar_defs
 val create_goal_evar_defs : evar_defs -> evar_defs
 val is_defined_evar :  evar_defs -> existential -> bool
 val subst_evar_map : substitution -> evar_defs -> evar_defs
+val unsafe_remove : evar_defs -> evar -> evar_defs
 (*** /Deprecaded ***)
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 06d1aa533b..ef154620f7 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -46,7 +46,7 @@ let precatchable_exception = function
     Nametab.GlobalizationError _ | PretypeError _)) -> true
   | _ -> false
 
-let nf_evar = Reductionops.nf_evar
+let nf_evar = Evd.nf_evar
 let j_nf_evar sigma j = 
   { uj_val = nf_evar sigma j.uj_val;
     uj_type = nf_evar sigma j.uj_type }
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index b6749db198..37b65cf907 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -311,7 +311,7 @@ let is_open_canonical_projection sigma (c,args) =
   try 
     let l = Refmap.find (global_of_constr c) !object_table in
     let n = (snd (List.hd l)).o_NPARAMS in
-    try isEvar (whd_evar sigma (List.nth args n)) with Failure _ -> false
+    try isEvar (Evd.whd_evar sigma (List.nth args n)) with Failure _ -> false
   with Not_found -> false
 
 let freeze () =
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 38ac3485b2..53b23af123 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -490,18 +490,6 @@ let whd_eta c = app_stack (local_whd_state_gen eta Evd.empty (c,empty_stack))
 (*                   Reduction Functions                                    *)
 (****************************************************************************)
 
-(* Replacing defined evars for error messages *)
-let rec whd_evar sigma c =
-  match kind_of_term c with
-    | Evar ev ->
-        (match safe_evar_value sigma ev with
-            Some c -> whd_evar sigma c
-          | None -> c)
-    | Sort s when is_sort_variable sigma s -> whd_sort_variable sigma c
-    | _ -> c
-
-let nf_evar =
-  local_strong whd_evar
 
 (* lazy reduction functions. The infos must be created for each term *)
 (* Note by HH [oct 08] : why would it be the job of clos_norm_flags to add
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 535101d743..902c314b53 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -91,11 +91,11 @@ val clos_norm_flags : Closure.RedFlags.reds -> reduction_function
 val nf_beta : local_reduction_function
 val nf_betaiota : local_reduction_function
 val nf_betadeltaiota : reduction_function
-val nf_evar : evar_map -> constr -> constr
+(* arnaud: val nf_evar : evar_map -> constr -> constr *)
 
 val nf_betaiota_preserving_vm_cast : reduction_function
 (* Lazy strategy, weak head reduction *)
-val whd_evar :  evar_map -> constr -> constr
+(* arnaud: val whd_evar :  evar_map -> constr -> constr*)
 val whd_beta : local_reduction_function
 val whd_betaiota : local_reduction_function
 val whd_betaiotazeta : local_reduction_function
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 3323c75b48..3f2d0b4251 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -125,7 +125,7 @@ let retype sigma metamap =
     | _ -> family_of_sort (decomp_sort env sigma (type_of env t))
 
   and type_of_global_reference_knowing_parameters env c args =
-    let argtyps = Array.map (fun c -> nf_evar sigma (type_of env c)) args in
+    let argtyps = Array.map (fun c -> Evd.nf_evar sigma (type_of env c)) args in
     match kind_of_term c with
     | Ind ind ->
       let (_,mip) = lookup_mind_specif env ind in
@@ -146,7 +146,7 @@ let type_of_global_reference_knowing_parameters env sigma c args =
   let _,_,_,f = retype sigma [] in f env c args
 
 let type_of_global_reference_knowing_conclusion env sigma c conclty =
-  let conclty = nf_evar sigma conclty in
+  let conclty = Evd.nf_evar sigma conclty in
   match kind_of_term c with
     | Ind ind ->
         let (_,mip) = Inductive.lookup_mind_specif env ind in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 0129c06c87..3b6d427aeb 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1427,7 +1427,7 @@ let solvable_by_tactic env evi (ev,args) src =
 let solve_remaining_evars env initial_sigma evd c =
   let evdref = ref (Typeclasses.resolve_typeclasses ~fail:true env evd) in
   let rec proc_rec c =
-    match kind_of_term (Reductionops.whd_evar ( !evdref) c) with
+    match kind_of_term (Evd.whd_evar ( !evdref) c) with
       | Evar (ev,args as k) when not (Evd.mem initial_sigma ev) ->
             let (loc,src) = evar_source ev !evdref in
 	    let sigma =  !evdref in
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index 520f9b6311..ec1bbafc25 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -260,7 +260,7 @@ let declare_instance (k:global_reference -> rel_context -> constr list -> unit)
   let (evm,gen) = List.fold_right
     (fun ev (evm,gen) -> 
        if Evd.is_defined evm ev 
-       then Evd.remove evm ev,gen 
+       then Evd.unsafe_remove evm ev,gen 
        else evm,(ev::gen))
     gen (evm,[]) in
 (*  msgnl(str"instance complète : ["++Util.prlist_with_sep (fun _ -> str";") Util.pr_int gen++str"] : "++spc()++pr_evar_defs evm);*)
@@ -268,7 +268,7 @@ let declare_instance (k:global_reference -> rel_context -> constr list -> unit)
   let (_,ctx,evm) = List.fold_left
     ( fun (i,ctx,evm) ev -> 
 	let ctx = (Anonymous,None,lift (-i) (Evd.evar_concl(Evd.find evm ev)))::ctx in
-	let evm = subst_evar_in_evm ev (mkRel i) (Evd.remove evm ev) in
+	let evm = subst_evar_in_evm ev (mkRel i) (Evd.unsafe_remove evm ev) in
 	(i-1,ctx,evm)
     ) (ngen,[],evm) gen in
   let fields = List.rev (Evd.fold ( fun ev evi l -> evar_definition evi::l ) evm []) in