diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/extratactics.ml4 | 4 | ||||
| -rw-r--r-- | ltac/rewrite.ml | 11 | ||||
| -rw-r--r-- | ltac/tauto.ml | 19 |
3 files changed, 21 insertions, 13 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 8ea60b39a..beaf778a6 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -747,14 +747,14 @@ let mkCaseEq a : unit Proofview.tactic = let case_eq_intros_rewrite x = Proofview.Goal.nf_enter { enter = begin fun gl -> - let n = nb_prod (Proofview.Goal.concl gl) in + let n = nb_prod (Tacmach.New.project gl) (EConstr.of_constr (Proofview.Goal.concl gl)) in (* Pp.msgnl (Printer.pr_lconstr x); *) Tacticals.New.tclTHENLIST [ mkCaseEq x; Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let hyps = Tacmach.New.pf_ids_of_hyps gl in - let n' = nb_prod concl in + let n' = nb_prod (Tacmach.New.project gl) (EConstr.of_constr concl) in let h = Tacmach.New.of_old (fun g -> fresh_id hyps (Id.of_string "heq") g) gl in Tacticals.New.tclTHENLIST [ Tacticals.New.tclDO (n'-n-1) intro; diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 217f5f42e..cd76d4746 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -1527,23 +1527,24 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul in Some (Some (evars, res, newt)) (** Insert a declaration after the last declaration it depends on *) -let rec insert_dependent env decl accu hyps = match hyps with +let rec insert_dependent env sigma decl accu hyps = match hyps with | [] -> List.rev_append accu [decl] | ndecl :: rem -> - if occur_var_in_decl env (NamedDecl.get_id ndecl) decl then + if occur_var_in_decl env sigma (NamedDecl.get_id ndecl) decl then List.rev_append accu (decl :: hyps) else - insert_dependent env decl (ndecl :: accu) rem + insert_dependent env sigma decl (ndecl :: accu) rem let assert_replacing id newt tac = let prf = Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in let ctx = Environ.named_context env in let after, before = List.split_when (NamedDecl.get_id %> Id.equal id) ctx in let nc = match before with | [] -> assert false - | d :: rem -> insert_dependent env (LocalAssum (NamedDecl.get_id d, newt)) [] after @ rem + | d :: rem -> insert_dependent env sigma (LocalAssum (NamedDecl.get_id d, newt)) [] after @ rem in let env' = Environ.reset_with_named_context (val_of_named_context nc) env in Refine.refine ~unsafe:false { run = begin fun sigma -> @@ -1616,7 +1617,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = | Some id -> (** Only consider variables not depending on [id] *) let ctx = Environ.named_context env in - let filter decl = not (occur_var_in_decl env id decl) in + let filter decl = not (occur_var_in_decl env sigma id decl) in let nctx = List.filter filter ctx in Environ.reset_with_named_context (Environ.val_of_named_context nctx) env in diff --git a/ltac/tauto.ml b/ltac/tauto.ml index 756958c2f..6eab003b5 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 |