Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGES

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

5 files changed, 14 insertions, 16 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 8b1c6dfc5c..d79910c99e 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -53,7 +53,7 @@ let cl_sigma ce = evars_of ce.env
 let subst_clenv sub clenv = 
   { templval = map_fl (subst_mps sub) clenv.templval;
     templtyp = map_fl (subst_mps sub) clenv.templtyp;
-    env = subst_evar_defs sub clenv.env;
+    env = subst_evar_defs_light sub clenv.env;
     templenv = clenv.templenv }
 
 let clenv_nf_meta clenv c = nf_meta clenv.env c
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 34f5a3c14f..66270c2b31 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -327,7 +327,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  solve_simple_eqn evar_conv_x env isevars (pbty,ev1,t2)
 	else
 	  (* Postpone the use of an heuristic *)
-	  add_conv_pb (pbty,applist(term1,l1),applist(term2,l2)) isevars,
+	  add_conv_pb (pbty,env,applist(term1,l1),applist(term2,l2)) isevars,
 	  true
 
     | Rigid _, Flexible ev2 ->
@@ -342,7 +342,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  solve_simple_eqn evar_conv_x env isevars (pbty,ev2,t1)
 	else
 	  (* Postpone the use of an heuristic *)
-	  add_conv_pb (pbty,applist(term1,l1),applist(term2,l2)) isevars,
+	  add_conv_pb (pbty,env,applist(term1,l1),applist(term2,l2)) isevars,
 	  true
 
     | MaybeFlexible flex1, Rigid _ ->
@@ -524,8 +524,7 @@ let first_order_unification env isevars pbty (term1,l1) (term2,l2) =
 let consider_remaining_unif_problems env isevars =
   let (isevars,pbs) = get_conv_pbs isevars (fun _ -> true) in
   List.fold_left
-    (fun (isevars,b as p) (pbty,t1,t2) ->
-      (* Pas le bon env pour le problème... *)
+    (fun (isevars,b as p) (pbty,env,t1,t2) ->
       if b then first_order_unification env isevars pbty 
 	(apprec_nohdbeta env isevars (whd_castappevar (evars_of isevars) t1))
 	(apprec_nohdbeta env isevars (whd_castappevar (evars_of isevars) t2))
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 6f50dc93fe..54e84db86f 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -598,7 +598,7 @@ let solve_pattern_eqn env l1 c =
  * ass.
  *)
 
-let status_changed lev (pbty,t1,t2) =
+let status_changed lev (pbty,_,t1,t2) =
   try 
     List.mem (head_evar t1) lev or List.mem (head_evar t2) lev
   with Failure _ ->
@@ -657,7 +657,7 @@ let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) =
 	  evar_define env ev1 t2 isevars in
     let (isevars,pbs) = get_conv_pbs isevars (status_changed lsp) in
     List.fold_left
-      (fun (isevars,b as p) (pbty,t1,t2) ->
+      (fun (isevars,b as p) (pbty,env,t1,t2) ->
 	if b then conv_algo env isevars pbty t1 t2 else p) (isevars,true)
       pbs
   with e when precatchable_exception e ->
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 2afe4601ff..a247b5b1ef 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -372,18 +372,17 @@ type hole_kind =
   | TomatchTypeParameter of inductive * int
 
 type conv_pb = Reduction.conv_pb
-type evar_constraint = conv_pb * constr * constr
+type evar_constraint = conv_pb * Environ.env * constr * constr
 type evar_defs =
     { evars : evar_map;
       conv_pbs : evar_constraint list;
       history : (existential_key * (loc * hole_kind)) list;
       metas : clbinding Metamap.t }
 
-let subst_evar_defs sub evd =
+let subst_evar_defs_light sub evd =
+  assert (evd.evars = (Evarmap.empty,UniverseMap.empty));
+  assert (evd.conv_pbs = []);
   { evd with
-    conv_pbs =
-      List.map (fun (k,t1,t2) ->(k,subst_mps sub t1,subst_mps sub t2))
-        evd.conv_pbs;
     metas = Metamap.map (map_clb (subst_mps sub)) evd.metas }
 
 let create_evar_defs sigma =
@@ -567,7 +566,7 @@ let pr_evar_map sigma =
 
 let pr_constraints pbs =
   h 0
-    (prlist_with_sep pr_fnl (fun (pbty,t1,t2) ->
+    (prlist_with_sep pr_fnl (fun (pbty,_,t1,t2) ->
       print_constr t1 ++ spc() ++
       str (match pbty with
 	| Reduction.CONV -> "=="
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 8b9c7fc677..ac1ed145af 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -120,8 +120,8 @@ val map_clb : (constr -> constr) -> clbinding -> clbinding
 (* Unification state *)
 type evar_defs
 
-(* Substitution is not applied to the [evar_map] *)
-val subst_evar_defs : substitution -> evar_defs -> evar_defs
+(* Assume empty [evar_map] and [conv_pbs] *)
+val subst_evar_defs_light : substitution -> evar_defs -> evar_defs
 
 (* create an [evar_defs] with empty meta map: *)
 val create_evar_defs : evar_map -> evar_defs
@@ -147,7 +147,7 @@ val evar_source : existential_key -> evar_defs -> loc * hole_kind
 
 (* Unification constraints *)
 type conv_pb = Reduction.conv_pb
-type evar_constraint = conv_pb * constr * constr
+type evar_constraint = conv_pb * Environ.env * constr * constr
 val add_conv_pb :  evar_constraint -> evar_defs -> evar_defs
 val get_conv_pbs : evar_defs -> (evar_constraint -> bool) -> 
   evar_defs * evar_constraint list