diff options
| author | Pierre-Marie Pédrot | 2016-10-30 17:53:07 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:20:30 +0100 |
| commit | 5143129baac805d3a49ac3ee9f3344c7a447634f (patch) | |
| tree | 60fd3fb22fc95474454a6a60f3a8715bf7d766d0 /ltac/tauto.ml | |
| parent | a42795cc1c2a8ed3efa9960af920ff7b16d928f0 (diff) | |
Termops API using EConstr.
Diffstat (limited to 'ltac/tauto.ml')
| -rw-r--r-- | ltac/tauto.ml | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/ltac/tauto.ml b/ltac/tauto.ml index 756958c2f0..6eab003b5c 100644 --- a/ltac/tauto.ml +++ b/ltac/tauto.ml @@ -16,6 +16,7 @@ open Tacexpr open Tacinterp open Util open Tacticals.New +open Proofview.Notations let tauto_plugin = "tauto" let () = Mltop.add_known_module tauto_plugin @@ -111,14 +112,16 @@ let split = Tactics.split_with_bindings false [Misctypes.NoBindings] (** Test *) let is_empty _ ist = - if is_empty_type (assoc_var "X1" ist) then idtac else fail + Proofview.tclEVARMAP >>= fun sigma -> + if is_empty_type sigma (assoc_var "X1" ist) then idtac else fail (* Strictly speaking, this exceeds the propositional fragment as it matches also equality types (and solves them if a reflexivity) *) let is_unit_or_eq _ ist = + Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let test = if flags.strict_unit then is_unit_type else is_unit_or_eq_type in - if test (assoc_var "X1" ist) then idtac else fail + if test sigma (assoc_var "X1" ist) then idtac else fail let bugged_is_binary t = isApp t && @@ -132,21 +135,23 @@ let bugged_is_binary t = (** Dealing with conjunction *) let is_conj _ ist = + Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let ind = assoc_var "X1" ist in if (not flags.binary_mode_bugged_detection || bugged_is_binary ind) && - is_conjunction + is_conjunction sigma ~strict:flags.strict_in_hyp_and_ccl ~onlybinary:flags.binary_mode ind then idtac else fail let flatten_contravariant_conj _ ist = + Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let typ = assoc_var "X1" ist in let c = assoc_var "X2" ist in let hyp = assoc_var "id" ist in - match match_with_conjunction + match match_with_conjunction sigma ~strict:flags.strict_in_contravariant_hyp ~onlybinary:flags.binary_mode typ with @@ -160,21 +165,23 @@ let flatten_contravariant_conj _ ist = (** Dealing with disjunction *) let is_disj _ ist = + Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let t = assoc_var "X1" ist in if (not flags.binary_mode_bugged_detection || bugged_is_binary t) && - is_disjunction + is_disjunction sigma ~strict:flags.strict_in_hyp_and_ccl ~onlybinary:flags.binary_mode t then idtac else fail let flatten_contravariant_disj _ ist = + Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let typ = assoc_var "X1" ist in let c = assoc_var "X2" ist in let hyp = assoc_var "id" ist in - match match_with_disjunction + match match_with_disjunction sigma ~strict:flags.strict_in_contravariant_hyp ~onlybinary:flags.binary_mode typ with |