Be more conservative and keep the use of eq_constr in pretyping/ functions.

5 files changed, 40 insertions, 21 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index c436fed2c..f8e959075 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -830,7 +830,7 @@ let first_order_unification ts env evd (ev1,l1) (term2,l2) =
 let choose_less_dependent_instance evk evd term args =
   let evi = Evd.find_undefined evd evk in
   let subst = make_pure_subst evi args in
-  let subst' = List.filter (fun (id,c) -> eq_constr evd c term) subst in
+  let subst' = List.filter (fun (id,c) -> Term.eq_constr c term) subst in
   match subst' with
   | [] -> None
   | (id, _) :: _ -> Some (Evd.define evk (mkVar id) evd)
@@ -840,7 +840,7 @@ let apply_on_subterm evdref f c t =
     (* By using eq_constr, we make an approximation, for instance, we *)
     (* could also be interested in finding a term u convertible to t *)
     (* such that c occurs in u *)
-    if eq_constr !evdref c t then f k
+    if e_eq_constr evdref c t then f k
     else
       match kind_of_term t with
       | Evar (evk,args) when Evd.is_undefined !evdref evk ->
@@ -1002,7 +1002,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
   let app_empty = Array.is_empty l1 && Array.is_empty l2 in
   match kind_of_term term1, kind_of_term term2 with
   | Evar (evk1,args1), (Rel _|Var _) when app_empty
-      && List.for_all (fun a -> eq_constr evd a term2 || isEvar a)
+      && List.for_all (fun a -> Term.eq_constr a term2 || isEvar a)
         (remove_instance_local_defs evd evk1 args1) ->
       (* The typical kind of constraint coming from pattern-matching return
          type inference *)
@@ -1010,7 +1010,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
       | Some evd -> Success evd
       | None -> UnifFailure (evd, ConversionFailed (env,term1,term2)))
   | (Rel _|Var _), Evar (evk2,args2) when app_empty
-      && List.for_all (fun a -> eq_constr evd a term1 || isEvar a)
+      && List.for_all (fun a -> Term.eq_constr a term1 || isEvar a)
         (remove_instance_local_defs evd evk2 args2) ->
       (* The typical kind of constraint coming from pattern-matching return
          type inference *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 4bffe3d1f..ba877d35c 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -495,7 +495,7 @@ let make_projectable_subst aliases sigma evi args =
             | Var id' ->
                 let idc = normalize_alias_var evar_aliases id' in
                 let sub = try Id.Map.find idc all with Not_found -> [] in
-                if List.exists (fun (c,_,_) -> eq_constr sigma a c) sub then
+                if List.exists (fun (c,_,_) -> Term.eq_constr a c) sub then
                   (rest,all,cstrs)
                 else
                   (rest,
@@ -648,15 +648,15 @@ let rec assoc_up_to_alias sigma aliases y yc = function
   | [] -> raise Not_found
   | (c,cc,id)::l ->
       let c' = whd_evar sigma c in
-      if eq_constr sigma y c' then id
+      if Term.eq_constr y c' then id
       else
         match l with
         | _ :: _ -> assoc_up_to_alias sigma aliases y yc l
         | [] ->
           (* Last chance, we reason up to alias conversion *)
           match (if c == c' then cc else normalize_alias_opt aliases c') with
-          | Some cc when eq_constr sigma yc cc -> id
-          | _ -> if eq_constr sigma yc c then id else raise Not_found
+          | Some cc when Term.eq_constr yc cc -> id
+          | _ -> if Term.eq_constr yc c then id else raise Not_found
 
 let rec find_projectable_vars with_evars aliases sigma y subst =
   let yc = normalize_alias aliases y in
@@ -1172,7 +1172,8 @@ type conv_fun_bool =
  * depend on these args). *)
 
 let solve_refl ?(can_drop=false) conv_algo env evd pbty evk argsv1 argsv2 =
-  if Array.equal (eq_constr evd) argsv1 argsv2 then evd else
+  let evdref = ref evd in
+  if Array.equal (e_eq_constr evdref) argsv1 argsv2 then !evdref else
   (* Filter and restrict if needed *)
   let args = Array.map2 (fun a1 a2 -> (a1, a2)) argsv1 argsv2 in
   let untypedfilter =
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index bd105c728..e49ed7b45 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1333,24 +1333,35 @@ let test_conversion env d pb t u =
   try conversion_gen env d pb t u; true
   with _ -> false
 
-let eq_constr d t u =
-  Term.eq_constr_univs d.universes.uctx_universes t u
+let eq_constr evd t u =
+  let b, c = Universes.eq_constr_univs_infer evd.universes.uctx_universes t u in
+    if b then 
+      try let evd' = add_universe_constraints evd c in evd', b
+      with Univ.UniverseInconsistency _ -> evd, false
+    else evd, b
+
+let e_eq_constr evdref t u =
+  let evd, b = eq_constr !evdref t u in
+    evdref := evd; b
+
+let eq_constr_test evd t u =
+  snd (eq_constr evd t u)
 
 let eq_named_context_val d ctx1 ctx2 = 
   ctx1 == ctx2 ||
     let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in
     let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
-      Id.equal i1 i2 && Option.equal (eq_constr d) c1 c2 && (eq_constr d) t1 t2
+      Id.equal i1 i2 && Option.equal (eq_constr_test d) c1 c2 && (eq_constr_test d) t1 t2
     in List.equal eq_named_declaration c1 c2
 
 let eq_evar_body d b1 b2 = match b1, b2 with
 | Evar_empty, Evar_empty -> true
-| Evar_defined t1, Evar_defined t2 -> eq_constr d t1 t2
+| Evar_defined t1, Evar_defined t2 -> eq_constr_test d t1 t2
 | _ -> false
 
 let eq_evar_info d ei1 ei2 =
   ei1 == ei2 ||
-    eq_constr d ei1.evar_concl ei2.evar_concl &&
+    eq_constr_test d ei1.evar_concl ei2.evar_concl &&
     eq_named_context_val d (ei1.evar_hyps) (ei2.evar_hyps) &&
     eq_evar_body d ei1.evar_body ei2.evar_body
     (** ppedrot: [eq_constr] may be a bit too permissive here *)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index d0a47fe96..b284bd42c 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -515,11 +515,18 @@ val fresh_global : ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map ->
 
 val conversion : env -> evar_map -> conv_pb -> constr -> constr -> evar_map
 
-(** This one forgets about the assignemts of universes. *)
 val test_conversion : env -> evar_map -> conv_pb -> constr -> constr -> bool
+(** This one forgets about the assignemts of universes. *)
+
+val eq_constr : evar_map -> constr -> constr -> evar_map * bool
+(** Syntactic equality up to universes, recording the associated constraints *)
+
+val e_eq_constr : evar_map ref -> constr -> constr -> bool
+(** Syntactic equality up to universes. *)
 
-(** Syntactic equality up to universe constraints. *)
-val eq_constr : evar_map -> constr -> constr -> bool
+val eq_constr_test : evar_map -> constr -> constr -> bool
+(** Syntactic equality up to universes, throwing away the (consistent) constraints
+    in case of success. *)
 
 (********************************************************************
    constr with holes *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 7530ced7c..7b302229b 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -717,11 +717,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
   and reduce curenvnb pb b wt (sigma, metas, evars as substn) cM cN =
     if use_full_betaiota flags && not (subterm_restriction b flags) then
       let cM' = do_reduce flags.modulo_delta curenvnb sigma cM in
-	if not (eq_constr sigma cM cM') then
+	if not (Term.eq_constr cM cM') then
 	  unirec_rec curenvnb pb b wt substn cM' cN
 	else
 	  let cN' = do_reduce flags.modulo_delta curenvnb sigma cN in
-	    if not (eq_constr sigma cN cN') then
+	    if not (Term.eq_constr cN cN') then
 	      unirec_rec curenvnb pb b wt substn cM cN'
 	    else error_cannot_unify (fst curenvnb) sigma (cM,cN)
     else error_cannot_unify (fst curenvnb) sigma (cM,cN)
@@ -1500,7 +1500,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
 let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) =
   let return a b =
     let (evd,c as a) = a () in
-      if List.exists (fun (evd',c') -> eq_constr evd' c c') b then b else a :: b
+      if List.exists (fun (evd',c') -> Term.eq_constr c c') b then b else a :: b
   in
   let fail str _ = error str in
   let bind f g a =
@@ -1577,7 +1577,7 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t =
         in
 	  if not flags.allow_K_in_toplevel_higher_order_unification &&
             (* ensure we found a different instance *)
-	    List.exists (fun op -> eq_constr evd op cl) l
+	    List.exists (fun op -> Term.eq_constr op cl) l
 	  then error_non_linear_unification env evd hdmeta cl
 	  else (evd',cl::l)
       else if flags.allow_K_in_toplevel_higher_order_unification