From 89a85a6603b7112e685a052d728284d3e4c2881e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Fri, 11 May 2018 23:07:14 +0200
Subject: Fix #7421: constr_eq ignores universe constraints.

The test isn't quite the one in #7421 because that use of algebraic
universes is wrong.
---
 tactics/tactics.ml  | 20 ++++++++++++++++++++
 tactics/tactics.mli |  5 +++++
 2 files changed, 25 insertions(+)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 770e31fea..c430edf2e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5034,6 +5034,26 @@ let tclABSTRACT ?(opaque=true) name_op tac =
     else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in
   abstract_subproof ~opaque s gk tac
 
+let constr_eq ~strict x y =
+  let fail = Tacticals.New.tclFAIL 0 (str "Not equal") in
+  let fail_universes = Tacticals.New.tclFAIL 0 (str "Not equal (due to universes)") in
+  Proofview.Goal.enter begin fun gl ->
+    let env = Tacmach.New.pf_env gl in
+    let evd = Tacmach.New.project gl in
+      match EConstr.eq_constr_universes env evd x y with
+      | Some csts ->
+        let csts = UnivProblem.to_constraints ~force_weak:false (Evd.universes evd) csts in
+        if strict then
+          if Evd.check_constraints evd csts then Proofview.tclUNIT ()
+          else fail_universes
+        else
+          (match Evd.add_constraints evd csts with
+           | evd -> Proofview.Unsafe.tclEVARS evd
+           | exception Univ.UniverseInconsistency _ ->
+             fail_universes)
+      | None -> fail
+  end
+
 let unify ?(state=full_transparent_state) x y =
   Proofview.Goal.enter begin fun gl ->
   let sigma = Proofview.Goal.sigma gl in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 8d4302450..57f20d2ff 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -409,6 +409,11 @@ val generalize_dep  : ?with_let:bool (** Don't lose let bindings *) -> constr  -
 
 (** {6 Other tactics. } *)
 
+(** Syntactic equality up to universes. With [strict] the universe
+   constraints must be already true to succeed, without [strict] they
+   are added to the evar map. *)
+val constr_eq : strict:bool -> constr -> constr -> unit Proofview.tactic
+
 val unify           : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic
 
 val cache_term_by_tactic_then : opaque:bool -> ?goal_type:(constr option) -> Id.t -> Decl_kinds.goal_kind -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic
-- 
cgit v1.2.3