diff options
| -rw-r--r-- | ltac/tauto.ml | 37 |
1 files changed, 15 insertions, 22 deletions
diff --git a/ltac/tauto.ml b/ltac/tauto.ml index e3f5342de..a4faf438a 100644 --- a/ltac/tauto.ml +++ b/ltac/tauto.ml @@ -7,6 +7,7 @@ (************************************************************************) open Term +open EConstr open Hipattern open Names open Pp @@ -24,7 +25,7 @@ let () = Mltop.add_known_module tauto_plugin let assoc_var s ist = let v = Id.Map.find (Names.Id.of_string s) ist.lfun in match Value.to_constr v with - | Some c -> c + | Some c -> EConstr.of_constr c | None -> failwith "tauto: anomaly" (** Parametrization of tauto *) @@ -113,7 +114,7 @@ let split = Tactics.split_with_bindings false [Misctypes.NoBindings] let is_empty _ ist = Proofview.tclEVARMAP >>= fun sigma -> - if is_empty_type sigma (EConstr.of_constr (assoc_var "X1" ist)) then idtac else fail + 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) *) @@ -121,13 +122,12 @@ 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 sigma (EConstr.of_constr (assoc_var "X1" ist)) then idtac else fail + if test sigma (assoc_var "X1" ist) then idtac else fail -let bugged_is_binary t = - let t = EConstr.Unsafe.to_constr t in - isApp t && - let (hdapp,args) = decompose_app t in - match (kind_of_term hdapp) with +let bugged_is_binary sigma t = + isApp sigma t && + let (hdapp,args) = decompose_app sigma t in + match EConstr.kind sigma hdapp with | Ind (ind,u) -> let (mib,mip) = Global.lookup_inductive ind in Int.equal mib.Declarations.mind_nparams 2 @@ -139,8 +139,7 @@ let is_conj _ ist = Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let ind = assoc_var "X1" ist in - let ind = EConstr.of_constr ind in - if (not flags.binary_mode_bugged_detection || bugged_is_binary ind) && + if (not flags.binary_mode_bugged_detection || bugged_is_binary sigma ind) && is_conjunction sigma ~strict:flags.strict_in_hyp_and_ccl ~onlybinary:flags.binary_mode ind @@ -151,7 +150,6 @@ let flatten_contravariant_conj _ ist = Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let typ = assoc_var "X1" ist in - let typ = EConstr.of_constr typ in let c = assoc_var "X2" ist in let hyp = assoc_var "id" ist in match match_with_conjunction sigma @@ -159,12 +157,10 @@ let flatten_contravariant_conj _ ist = ~onlybinary:flags.binary_mode typ with | Some (_,args) -> - let args = List.map EConstr.Unsafe.to_constr args in let newtyp = List.fold_right mkArrow args c in - let newtyp = EConstr.of_constr newtyp in let intros = tclMAP (fun _ -> intro) args in - let by = tclTHENLIST [intros; apply (EConstr.of_constr hyp); split; assumption] in - tclTHENLIST [assert_ ~by newtyp; clear (destVar hyp)] + let by = tclTHENLIST [intros; apply hyp; split; assumption] in + tclTHENLIST [assert_ ~by newtyp; clear (destVar sigma hyp)] | _ -> fail (** Dealing with disjunction *) @@ -173,8 +169,7 @@ let is_disj _ ist = Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let t = assoc_var "X1" ist in - let t = EConstr.of_constr t in - if (not flags.binary_mode_bugged_detection || bugged_is_binary t) && + if (not flags.binary_mode_bugged_detection || bugged_is_binary sigma t) && is_disjunction sigma ~strict:flags.strict_in_hyp_and_ccl ~onlybinary:flags.binary_mode t @@ -185,9 +180,7 @@ let flatten_contravariant_disj _ ist = Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let typ = assoc_var "X1" ist in - let typ = EConstr.of_constr typ in let c = assoc_var "X2" ist in - let c = EConstr.of_constr c in let hyp = assoc_var "id" ist in match match_with_disjunction sigma ~strict:flags.strict_in_contravariant_hyp @@ -195,13 +188,13 @@ let flatten_contravariant_disj _ ist = typ with | Some (_,args) -> let map i arg = - let typ = EConstr.mkArrow arg c in + let typ = mkArrow arg c in let ci = Tactics.constructor_tac false None (succ i) Misctypes.NoBindings in - let by = tclTHENLIST [intro; apply (EConstr.of_constr hyp); ci; assumption] in + let by = tclTHENLIST [intro; apply hyp; ci; assumption] in assert_ ~by typ in let tacs = List.mapi map args in - let tac0 = clear (destVar hyp) in + let tac0 = clear (destVar sigma hyp) in tclTHEN (tclTHENLIST tacs) tac0 | _ -> fail |