From 81107b12644c78f204d0a46df520b8b2d8e72142 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 26 Apr 2018 14:25:30 +0200 Subject: Deprecate Evarconv.e_conv,e_cumul --- plugins/funind/functional_principles_proofs.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 8da0e1c4f..a0616b308 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -243,7 +243,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = raise NoChange; end in - let eq_constr c1 c2 = Evarconv.e_conv env (ref sigma) c1 c2 in + let eq_constr c1 c2 = Option.has_some (Evarconv.conv env sigma c1 c2) 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