diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-26 14:25:30 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-11 13:41:26 +0200 |
commit | 81107b12644c78f204d0a46df520b8b2d8e72142 (patch) | |
tree | 85b9575ade7ce2dffff6ee66a652706c82b34d2c /plugins/funind | |
parent | c538b7fd555828d9fba9ea97503fac6c70377b76 (diff) |
Deprecate Evarconv.e_conv,e_cumul
Diffstat (limited to 'plugins/funind')
-rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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"; |