diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extratactics.ml4 | 2 | ||||
| -rw-r--r-- | tactics/g_rewrite.ml4 | 15 | ||||
| -rw-r--r-- | tactics/leminv.ml | 4 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 9 | ||||
| -rw-r--r-- | tactics/rewrite.mli | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 7 |
6 files changed, 19 insertions, 20 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index a383b14528..9edf6302da 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -785,5 +785,5 @@ END;; VERNAC COMMAND EXTEND GrabEvars [ "Grab" "Existential" "Variables" ] => [ Vernacexpr.VtProofStep, Vernacexpr.VtLater ] - -> [ Proof_global.with_current_proof (fun _ p -> Proof.V82.grab_evars p) ] + -> [ Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p) ] END diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4 index f889f9cb2c..846bba1d46 100644 --- a/tactics/g_rewrite.ml4 +++ b/tactics/g_rewrite.ml4 @@ -146,21 +146,20 @@ TACTIC EXTEND setoid_rewrite [ Proofview.V82.tactic (cl_rewrite_clause c o (occurrences_of occ) (Some id))] END -let cl_rewrite_clause_newtac_tac c o occ cl gl = - cl_rewrite_clause_newtac' c o occ cl; - tclIDTAC gl +let cl_rewrite_clause_newtac_tac c o occ cl = + cl_rewrite_clause_newtac' c o occ cl TACTIC EXTEND GenRew | [ "rew" orient(o) glob_constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ) ] -> - [ Proofview.V82.tactic (cl_rewrite_clause_newtac_tac c o (occurrences_of occ) (Some id)) ] + [ cl_rewrite_clause_newtac_tac c o (occurrences_of occ) (Some id) ] | [ "rew" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id) ] -> - [ Proofview.V82.tactic (cl_rewrite_clause_newtac_tac c o (occurrences_of occ) (Some id)) ] + [ cl_rewrite_clause_newtac_tac c o (occurrences_of occ) (Some id) ] | [ "rew" orient(o) glob_constr_with_bindings(c) "in" hyp(id) ] -> - [ Proofview.V82.tactic (cl_rewrite_clause_newtac_tac c o AllOccurrences (Some id)) ] + [ cl_rewrite_clause_newtac_tac c o AllOccurrences (Some id) ] | [ "rew" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) ] -> - [ Proofview.V82.tactic (cl_rewrite_clause_newtac_tac c o (occurrences_of occ) None) ] + [ cl_rewrite_clause_newtac_tac c o (occurrences_of occ) None ] | [ "rew" orient(o) glob_constr_with_bindings(c) ] -> - [ Proofview.V82.tactic (cl_rewrite_clause_newtac_tac c o AllOccurrences None) ] + [ cl_rewrite_clause_newtac_tac c o AllOccurrences None ] END VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 06b067fcf4..04819830e5 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -198,8 +198,8 @@ let inversion_scheme env sigma t sort dep_option inv_op = *) let pf = Proof.start [invEnv,invGoal] in let pf = - Proof.run_tactic env ( - Tacticals.New.tclTHEN intro (Tacticals.New.onLastHypId inv_op)) pf + fst (Proof.run_tactic env ( + Tacticals.New.tclTHEN intro (Tacticals.New.onLastHypId inv_op)) pf) in let pfterm = List.hd (Proof.partial_proof pf) in let global_named_context = Global.named_context () in diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 30fe8d4aef..66b2c64b0f 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -361,7 +361,7 @@ let solve_remaining_by by env prf = let evd' = List.fold_right (fun mv evd -> let ty = Clenv.clenv_nf_meta env (meta_type evd mv) in - let c = Pfedit.build_by_tactic env.env ty (Tacticals.New.tclCOMPLETE tac) in + let c,_ = Pfedit.build_by_tactic env.env ty (Tacticals.New.tclCOMPLETE tac) in meta_assign mv (c, (Conv,TypeNotProcessed)) evd) indep env.evd in { env with evd = evd' }, prf @@ -1342,9 +1342,8 @@ let cl_rewrite_clause_new_strat ?abs strat clause = newfail 0 (str"setoid rewrite failed: " ++ s)) let cl_rewrite_clause_newtac' l left2right occs clause = - Proof_global.with_current_proof (fun _ -> Proof.run_tactic (Global.env ()) - (Proofview.tclFOCUS 1 1 - (cl_rewrite_clause_new_strat (rewrite_with rewrite_unif_flags l left2right occs) clause))) + Proofview.tclFOCUS 1 1 + (cl_rewrite_clause_new_strat (rewrite_with rewrite_unif_flags l left2right occs) clause) let cl_rewrite_clause_strat strat clause = tclTHEN (tactic_init_setoid ()) @@ -1641,7 +1640,7 @@ let add_morphism_infer glob m n = glob (ConstRef cst)); declare_projection n instance_id (ConstRef cst) | _ -> assert false); - Pfedit.by (Tacinterp.interp tac)) () + ignore (Pfedit.by (Tacinterp.interp tac))) () let add_morphism glob binders m s n = init_setoid (); diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli index 637bab5a6a..63166c64a5 100644 --- a/tactics/rewrite.mli +++ b/tactics/rewrite.mli @@ -43,7 +43,7 @@ val cl_rewrite_clause : val cl_rewrite_clause_newtac' : interp_sign * (glob_constr_and_expr * glob_constr_and_expr bindings) -> - bool -> Locus.occurrences -> Id.t option -> unit + bool -> Locus.occurrences -> Id.t option -> unit Proofview.tactic val is_applied_rewrite_relation : env -> evar_map -> Context.rel_context -> constr -> types option diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5b1ae69e33..4026b42587 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3740,7 +3740,8 @@ let abstract_subproof id tac gl = try flush_and_check_evars (project gl) concl with Uninstantiated_evar _ -> error "\"abstract\" cannot handle existentials." in - let const = Pfedit.build_constant_by_tactic id secsign concl + (* spiwack: the [abstract] tacticals loses the "unsafe status" information *) + let (const,_) = Pfedit.build_constant_by_tactic id secsign concl (Tacticals.New.tclCOMPLETE (Tacticals.New.tclTHEN (Tacticals.New.tclDO (List.length sign) intro) tac)) in let cd = Entries.DefinitionEntry const in let decl = (cd, IsProof Lemma) in @@ -3764,9 +3765,9 @@ let tclABSTRACT name_op tac gl = let admit_as_an_axiom = - (* spiwack: admit temporarily won't report an unsafe status *) Proofview.tclUNIT () >= fun () -> (* delay for Coqlib.build_coq_proof_admitted *) - simplest_case (Coqlib.build_coq_proof_admitted ()) + simplest_case (Coqlib.build_coq_proof_admitted ()) <*> + Proofview.mark_as_unsafe let unify ?(state=full_transparent_state) x y gl = try |