From 89a85a6603b7112e685a052d728284d3e4c2881e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
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.mli | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'tactics/tactics.mli')

diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 8d43024507..57f20d2ff2 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