From b365304d32db443194b7eaadda63c784814f53f1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Nov 2016 03:23:13 +0100 Subject: Evarconv API using EConstr. --- plugins/funind/functional_principles_proofs.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind/functional_principles_proofs.ml') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 258ee5ad6..340dd2c28 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -237,7 +237,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type = failwith "NoChange"; end in - let eq_constr = Evarconv.e_conv env (ref sigma) in + let eq_constr c1 c2 = Evarconv.e_conv env (ref sigma) (EConstr.of_constr c1) (EConstr.of_constr c2) in if not (noccurn 1 end_of_type) then nochange "dependent"; (* if end_of_type depends on this term we don't touch it *) if not (isApp t) then nochange "not an equality"; -- cgit v1.2.3