aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/evarconv.ml8
-rw-r--r--pretyping/evarsolve.ml12
-rw-r--r--pretyping/evd.ml36
-rw-r--r--pretyping/evd.mli8
-rw-r--r--pretyping/patternops.ml4
-rw-r--r--pretyping/unification.ml10
-rw-r--r--proofs/clenv.ml4
-rw-r--r--proofs/goal.ml2
-rw-r--r--tactics/auto.ml8
-rw-r--r--tactics/class_tactics.ml5
-rw-r--r--tactics/equality.ml6
-rw-r--r--tactics/extratactics.ml49
-rw-r--r--tactics/tactics.ml21
-rw-r--r--test-suite/bugs/closed/3593.v10
-rw-r--r--toplevel/himsg.ml4
15 files changed, 89 insertions, 58 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 0fd508604..c436fed2c 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 c term) subst in
+ let subst' = List.filter (fun (id,c) -> eq_constr evd 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 c t then f k
+ if 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 a term2 || isEvar a)
+ && List.for_all (fun a -> eq_constr evd 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 a term1 || isEvar a)
+ && List.for_all (fun a -> eq_constr evd 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 f32238ee7..4bffe3d1f 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -351,7 +351,7 @@ let rec expand_and_check_vars aliases = function
module Constrhash = Hashtbl.Make
(struct type t = constr
- let equal = eq_constr
+ let equal = Term.eq_constr
let hash = hash_constr
end)
@@ -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 a c) sub then
+ if List.exists (fun (c,_,_) -> eq_constr sigma 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 y c' then id
+ if eq_constr sigma 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 yc cc -> id
- | _ -> if eq_constr yc c then id else raise Not_found
+ | Some cc when eq_constr sigma yc cc -> id
+ | _ -> if eq_constr sigma 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,7 @@ 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 argsv1 argsv2 then evd else
+ if Array.equal (eq_constr evd) argsv1 argsv2 then evd 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 aa2ca0009..bd105c728 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -198,19 +198,6 @@ let evar_filtered_env evi = match Filter.repr (evar_filter evi) with
in
make_env filter (evar_context evi)
-let eq_evar_body b1 b2 = match b1, b2 with
-| Evar_empty, Evar_empty -> true
-| Evar_defined t1, Evar_defined t2 -> eq_constr t1 t2
-| _ -> false
-
-let eq_evar_info ei1 ei2 =
- ei1 == ei2 ||
- eq_constr ei1.evar_concl ei2.evar_concl &&
- eq_named_context_val (ei1.evar_hyps) (ei2.evar_hyps) &&
- eq_evar_body ei1.evar_body ei2.evar_body
- (** ppedrot: [eq_constr] may be a bit too permissive here *)
-
-
let map_evar_body f = function
| Evar_empty -> Evar_empty
| Evar_defined d -> Evar_defined (f d)
@@ -1346,6 +1333,29 @@ 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_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
+ 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
+| _ -> false
+
+let eq_evar_info d ei1 ei2 =
+ ei1 == ei2 ||
+ eq_constr 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 *)
+
+
(**********************************************************)
(* Accessing metas *)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index bbae32d8c..d0a47fe96 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -103,8 +103,6 @@ type evar_info = {
(** Extra store, used for clever hacks. *)
}
-val eq_evar_info : evar_info -> evar_info -> bool
-
val make_evar : named_context_val -> types -> evar_info
val evar_concl : evar_info -> constr
val evar_context : evar_info -> named_context
@@ -214,6 +212,9 @@ val add_constraints : evar_map -> Univ.constraints -> evar_map
val undefined_map : evar_map -> evar_info Evar.Map.t
(** Access the undefined evar mapping directly. *)
+val eq_evar_info : evar_map -> evar_info -> evar_info -> bool
+(** Compare the evar_info's up to the universe constraints of the evar map. *)
+
(** {6 Instantiating partial terms} *)
exception NotInstantiatedEvar
@@ -517,6 +518,9 @@ 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
+(** Syntactic equality up to universe constraints. *)
+val eq_constr : evar_map -> constr -> constr -> bool
+
(********************************************************************
constr with holes *)
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 54ce29bf7..44ff2b5b8 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -75,8 +75,8 @@ and cofixpoint_eq (i1, r1) (i2, r2) =
and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) =
Array.equal Name.equal n1 n2 &&
- Array.equal eq_constr c1 c2 &&
- Array.equal eq_constr r1 r2
+ Array.equal Term.eq_constr c1 c2 &&
+ Array.equal Term.eq_constr r1 r2
let rec occur_meta_pattern = function
| PApp (f,args) ->
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 937d84972..7530ced7c 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -389,7 +389,7 @@ let expand_key ts env sigma = function
| Some (IsProj (p, c)) ->
let red = Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma
Cst_stack.empty (c, unfold_projection env p [])))
- in if eq_constr (mkProj (p, c)) red then None else Some red
+ in if Term.eq_constr (mkProj (p, c)) red then None else Some red
| None -> None
let subterm_restriction is_subterm flags =
@@ -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 cM cM') then
+ if not (eq_constr sigma 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 cN cN') then
+ if not (eq_constr sigma 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 c c') b then b else a :: b
+ if List.exists (fun (evd',c') -> eq_constr evd' 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 op cl) l
+ List.exists (fun op -> eq_constr evd 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
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 612ef8d7d..5a7572eb2 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -167,7 +167,7 @@ let clenv_assign mv rhs clenv =
error "clenv_assign: circularity in unification";
try
if meta_defined clenv.evd mv then
- if not (eq_constr (fst (meta_fvalue clenv.evd mv)).rebus rhs) then
+ if not (eq_constr clenv.evd (fst (meta_fvalue clenv.evd mv)).rebus rhs) then
error_incompatible_inst clenv mv
else
clenv
@@ -480,7 +480,7 @@ let clenv_match_args bl clenv =
(fun clenv (loc,b,c) ->
let k = meta_of_binder clenv loc mvs b in
if meta_defined clenv.evd k then
- if eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv
+ if eq_constr clenv.evd (fst (meta_fvalue clenv.evd k)).rebus c then clenv
else error_already_defined b
else
clenv_assign_binding clenv k c)
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 55de87261..dea704a68 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -94,7 +94,7 @@ let solution sigma g =
let equal evars1 gl1 evars2 gl2 =
let evi1 = content evars1 gl1 in
let evi2 = content evars2 gl2 in
- Evd.eq_evar_info evi1 evi2
+ Evd.eq_evar_info evars2 evi1 evi2
(* [contained_in_info e evi] checks whether the evar [e] appears in
the hypotheses, the conclusion or the body of the evar_info
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0f1d7cb02..6fa4342d3 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -146,14 +146,14 @@ let eq_pri_auto_tactic (_, x) (_, y) =
if Int.equal x.pri y.pri && Option.equal constr_pattern_eq x.pat y.pat then
match x.code,y.code with
| Res_pf (cstr,_),Res_pf (cstr1,_) ->
- eq_constr cstr cstr1
+ Term.eq_constr cstr cstr1
| ERes_pf (cstr,_),ERes_pf (cstr1,_) ->
- eq_constr cstr cstr1
+ Term.eq_constr cstr cstr1
| Give_exact (cstr,_),Give_exact (cstr1,_) ->
- eq_constr cstr cstr1
+ Term.eq_constr cstr cstr1
| Res_pf_THEN_trivial_fail (cstr,_)
,Res_pf_THEN_trivial_fail (cstr1,_) ->
- eq_constr cstr cstr1
+ Term.eq_constr cstr cstr1
| _,_ -> false
else
false
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 7de9330ba..881bb5c62 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -249,7 +249,7 @@ let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
| _ ->
let env' = Environ.push_rel_context ctx env in
let ty' = whd_betadeltaiota env' ar in
- if not (eq_constr ty' ar) then iscl env' ty'
+ if not (Term.eq_constr ty' ar) then iscl env' ty'
else false
in
let is_class = iscl env cty in
@@ -278,13 +278,14 @@ let pf_filtered_hyps gls =
Goal.V82.hyps gls.Evd.sigma (sig_it gls)
let make_hints g st only_classes sign =
+ let sigma = project g in
let paths, hintlist =
List.fold_left
(fun (paths, hints) hyp ->
let consider =
try let (_, b, t) = Global.lookup_named (pi1 hyp) in
(* Section variable, reindex only if the type changed *)
- not (eq_constr t (pi3 hyp))
+ not (eq_constr sigma t (pi3 hyp))
with Not_found -> true
in
if consider then
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 4020a93fd..c524e67ce 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1588,8 +1588,8 @@ let is_eq_x gl x (id,_,c) =
try
let c = pf_nf_evar gl c in
let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in
- if (eq_constr x lhs) && not (occur_term x rhs) then raise (FoundHyp (id,rhs,true));
- if (eq_constr x rhs) && not (occur_term x lhs) then raise (FoundHyp (id,lhs,false))
+ if (Term.eq_constr x lhs) && not (occur_term x rhs) then raise (FoundHyp (id,rhs,true));
+ if (Term.eq_constr x rhs) && not (occur_term x lhs) then raise (FoundHyp (id,lhs,false))
with ConstrMatching.PatternMatchingFailure ->
()
@@ -1679,7 +1679,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
if flags.only_leibniz then restrict_to_eq_and_identity eq;
(* J.F.: added to prevent failure on goal containing x=x as an hyp *)
- if eq_constr x y then failwith "caught";
+ if Term.eq_constr x y then failwith "caught";
match kind_of_term x with Var x -> x | _ ->
match kind_of_term y with Var y -> y | _ -> failwith "caught"
with ConstrMatching.PatternMatchingFailure -> failwith "caught"
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 41f8dc8de..c1e6f42f1 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -777,9 +777,14 @@ END
(* ********************************************************************* *)
+let eq_constr x y =
+ Proofview.Goal.enter (fun gl ->
+ let evd = Proofview.Goal.sigma gl in
+ if Evd.eq_constr evd x y then Proofview.tclUNIT ()
+ else Tacticals.New.tclFAIL 0 (str "Not equal"))
+
TACTIC EXTEND constr_eq
-| [ "constr_eq" constr(x) constr(y) ] -> [
- if eq_constr x y then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "Not equal") ]
+| [ "constr_eq" constr(x) constr(y) ] -> [ eq_constr x y ]
END
TACTIC EXTEND constr_eq_nounivs
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a495c8783..28e0b7262 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1124,7 +1124,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
let hypclause = mk_clenv_from_env env sigma (Some 0) (hyp, hyp_typ) in
let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in
let new_hyp_typ = clenv_type elimclause'' in
- if eq_constr hyp_typ new_hyp_typ then
+ if eq_constr sigma hyp_typ new_hyp_typ then
errorlabstrm "general_rewrite_in"
(str "Nothing to rewrite in " ++ pr_id id ++ str".");
clenv_refine_in with_evars id id sigma elimclause''
@@ -3065,14 +3065,14 @@ let specialize_eqs id gl =
match kind_of_term ty with
| Prod (na, t, b) ->
(match kind_of_term t with
- | App (eq, [| eqty; x; y |]) when eq_constr (Lazy.force coq_eq) eq ->
+ | App (eq, [| eqty; x; y |]) when eq_constr !evars (Lazy.force coq_eq) eq ->
let c = if noccur_between 1 (List.length ctx) x then y else x in
let pt = mkApp (Lazy.force coq_eq, [| eqty; c; c |]) in
let p = mkApp (Lazy.force coq_eq_refl, [| eqty; c |]) in
if unif (push_rel_context ctx env) evars pt t then
aux true ctx (mkApp (acc, [| p |])) (subst1 p b)
else acc, in_eqs, ctx, ty
- | App (heq, [| eqty; x; eqty'; y |]) when eq_constr heq (Lazy.force coq_heq) ->
+ | App (heq, [| eqty; x; eqty'; y |]) when eq_constr !evars heq (Lazy.force coq_heq) ->
let eqt, c = if noccur_between 1 (List.length ctx) x then eqty', y else eqty, x in
let pt = mkApp (Lazy.force coq_heq, [| eqt; c; eqt; c |]) in
let p = mkApp (Lazy.force coq_heq_refl, [| eqt; c |]) in
@@ -3262,16 +3262,16 @@ let compute_scheme_signature scheme names_info ind_type_guess =
| Some (_,Some _,_) ->
error "Strange letin, cannot recognize an induction scheme."
| None -> (* Non standard scheme *)
- let cond hd = eq_constr hd ind_type_guess && not scheme.farg_in_concl
+ let cond hd = Term.eq_constr hd ind_type_guess && not scheme.farg_in_concl
in (cond, fun _ _ -> ())
| Some ( _,None,ind) -> (* Standard scheme from an inductive type *)
let indhd,indargs = decompose_app ind in
- let cond hd = eq_constr hd indhd in
+ let cond hd = Term.eq_constr hd indhd in
let check_concl is_pred p =
(* Check again conclusion *)
let ccl_arg_ok = is_pred (p + scheme.nargs + 1) f == IndArg in
let ind_is_ok =
- List.equal eq_constr
+ List.equal Term.eq_constr
(List.lastn scheme.nargs indargs)
(extended_rel_list 0 scheme.args) in
if not (ccl_arg_ok && ind_is_ok) then
@@ -4030,10 +4030,10 @@ let intros_transitivity n = Tacticals.New.tclTHEN intros (transitivity_gen n)
is solved by tac *)
(** d1 is the section variable in the global context, d2 in the goal context *)
-let interpretable_as_section_decl d1 d2 = match d2,d1 with
+let interpretable_as_section_decl evd d1 d2 = match d2,d1 with
| (_,Some _,_), (_,None,_) -> false
- | (_,Some b1,t1), (_,Some b2,t2) -> eq_constr b1 b2 && eq_constr t1 t2
- | (_,None,t1), (_,_,t2) -> eq_constr t1 t2
+ | (_,Some b1,t1), (_,Some b2,t2) -> eq_constr evd b1 b2 && eq_constr evd t1 t2
+ | (_,None,t1), (_,_,t2) -> eq_constr evd t1 t2
let abstract_subproof id gk tac =
let open Tacticals.New in
@@ -4042,11 +4042,12 @@ let abstract_subproof id gk tac =
Proofview.Goal.nf_enter begin fun gl ->
let current_sign = Global.named_context()
and global_sign = Proofview.Goal.hyps gl in
+ let sigma = Proofview.Goal.sigma gl in
let sign,secsign =
List.fold_right
(fun (id,_,_ as d) (s1,s2) ->
if mem_named_context id current_sign &&
- interpretable_as_section_decl (Context.lookup_named id current_sign) d
+ interpretable_as_section_decl sigma (Context.lookup_named id current_sign) d
then (s1,push_named_context_val d s2)
else (add_named_decl d s1,s2))
global_sign (empty_named_context,empty_named_context_val) in
diff --git a/test-suite/bugs/closed/3593.v b/test-suite/bugs/closed/3593.v
new file mode 100644
index 000000000..25f9db6b2
--- /dev/null
+++ b/test-suite/bugs/closed/3593.v
@@ -0,0 +1,10 @@
+Set Universe Polymorphism.
+Set Printing All.
+Set Implicit Arguments.
+Record prod A B := pair { fst : A ; snd : B }.
+Goal forall x : prod Set Set, let f := @fst _ in f _ x = @fst _ _ x.
+simpl; intros.
+ constr_eq (@fst Set Set x) (fst (A := Set) (B := Set) x).
+ Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x).
+ reflexivity.
+Qed.
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 5f7a7c353..6994c366c 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -277,11 +277,11 @@ let explain_unification_error env sigma p1 p2 = function
| NotSameArgSize | NotSameHead | NoCanonicalStructure ->
(* Error speaks from itself *) mt ()
| ConversionFailed (env,t1,t2) ->
- if eq_constr t1 p1 && eq_constr t2 p2 then mt () else
+ if eq_constr sigma t1 p1 && eq_constr sigma t2 p2 then mt () else
let env = make_all_name_different env in
let t1 = Evarutil.nf_evar sigma t1 in
let t2 = Evarutil.nf_evar sigma t2 in
- if not (eq_constr t1 p1) || not (eq_constr t2 p2) then
+ if not (eq_constr sigma t1 p1) || not (eq_constr sigma t2 p2) then
let t1, t2 = pr_explicit env sigma t1 t2 in
spc () ++ str "(cannot unify " ++ t1 ++ strbrk " and " ++
t2 ++ str ")"
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 08:21:48 +0000