From 78b51f541d0107f06c21fc1260aae2ab9f7229c5 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 17 Oct 2018 18:04:35 +0200
Subject: Change interfaces of evarconv as suggested by Enrico.

Now the main functions are unify (solves the problems entirely) and
unify_delay and unify_leq (which might leave some unsolved constraints).

Deprecated the_conv_x and the_conv_x_leq (which were misnommers as they
do unification not conversion).
---
 plugins/funind/functional_principles_proofs.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 8da30bd9c9..6fd2f7c2bc 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -238,7 +238,9 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
       raise NoChange;
     end
   in
-  let eq_constr c1 c2 = Option.has_some (Evarconv.conv env sigma c1 c2) in
+  let eq_constr c1 c2 =
+    try ignore(Evarconv.unify_delay env sigma c1 c2); true
+    with Evarconv.UnableToUnify _ -> false in
   if not (noccurn sigma 1 end_of_type)
   then nochange "dependent"; (* if end_of_type depends on this term we don't touch it  *)
     if not (isApp sigma t) then nochange "not an equality";
-- 
cgit v1.2.3