Unification: Fixing bug in materialize_evar (spotted by MathClasses).

Also fixed apparent other bug in the presence of let-ins.

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

1 files changed, 17 insertions, 17 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 00501a893..c509fe9da 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -822,12 +822,13 @@ let make_pure_subst evi args =
  * declares x1:T1..xq:Tq |- ?e : s such that ?e[u1..uq] = t holds.
  *)
 
-let define_evar_from_virtual_equation define_fun env evd t_in_env sign filter inst_in_env
-    inst_in_sign =
+let define_evar_from_virtual_equation define_fun env evd t_in_env sign filter inst_in_env =
   let ty_t_in_env = Retyping.get_type_of env evd t_in_env in
   let evd,evar_in_env = new_evar_instance sign evd ty_t_in_env ~filter inst_in_env in
   let t_in_env = whd_evar evd t_in_env in
   let evd = define_fun env evd (destEvar evar_in_env) t_in_env in
+  let ids = List.map pi1 (named_context_of_val sign) in
+  let inst_in_sign = List.map mkVar (list_filter_with filter ids) in
   let evar_in_sign = mkEvar (fst (destEvar evar_in_env), Array.of_list inst_in_sign) in
   (evd,whd_evar evd evar_in_sign)
 
@@ -857,27 +858,26 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
   let inst_in_sign = List.map mkVar (list_filter_with filter1 ids1) in
   let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) =
     List.fold_right (fun (na,b,t_in_env as d) (sign,filter,inst_in_env,inst_in_sign,env,evd,avoid) ->
-      match b with
-      | None ->
-          let id = next_name_away na avoid in
-          let evd,t_in_sign =
-            define_evar_from_virtual_equation define_fun env evd t_in_env
-              sign filter inst_in_env inst_in_sign in
-          (push_named_context_val (id,None,t_in_sign) sign,true::filter,
-           (mkRel 1)::(List.map (lift 1) inst_in_env),
-           (mkRel 1)::(List.map (lift 1) inst_in_sign),
-           push_rel d env,evd,id::avoid)
+      let id = next_name_away na avoid in
+      let evd,t_in_sign =
+        define_evar_from_virtual_equation define_fun env evd t_in_env
+          sign filter inst_in_env in
+      let evd,b_in_sign = match b with
+      | None -> evd,None
       | Some b ->
-          (sign,filter,
-           List.map (lift 1) inst_in_env,
-           List.map (lift 1) inst_in_sign,
-           push_rel d env,evd,avoid))
+          let evd,b = define_evar_from_virtual_equation define_fun env evd b
+            sign filter inst_in_env in
+          evd,Some b in
+      (push_named_context_val (id,b_in_sign,t_in_sign) sign,true::filter,
+       (mkRel 1)::(List.map (lift 1) inst_in_env),
+       (mkRel 1)::(List.map (lift 1) inst_in_sign),
+       push_rel d env,evd,id::avoid))
       rel_sign
       (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,ids1)
   in
   let evd,ev2ty_in_sign =
     define_evar_from_virtual_equation define_fun env evd ty_in_env
-      sign2 filter2 inst2_in_env inst2_in_sign in
+      sign2 filter2 inst2_in_env in
   let evd,ev2_in_sign =
     new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 inst2_in_sign in
   let ev2_in_env = (fst (destEvar ev2_in_sign), Array.of_list inst2_in_env) in