diff options
| author | Pierre-Marie Pédrot | 2016-05-17 22:37:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-17 22:38:40 +0200 |
| commit | f7fb1918619fcef384d4aa84938246de67c707fa (patch) | |
| tree | 6f8b1b8ba71681b06b4a74ddeee76d02a3ef09dd /plugins/decl_mode | |
| parent | cead0ce54cf290016e088ee7f203d327a3eea957 (diff) | |
| parent | dadd4003b6607ccc103658f842b5efbd6d8ab57f (diff) | |
Putting all the tactics exported by the Tactics module in the new monad API.
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 26 |
1 files changed, 21 insertions, 5 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 090b293f5c..be6ce59bd3 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -34,6 +34,22 @@ open Context.Named.Declaration (* Strictness option *) +let clear ids { it = goal; sigma } = + let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in + let env = Goal.V82.env sigma goal in + let sign = Goal.V82.hyps sigma goal in + let cl = Goal.V82.concl sigma goal in + let evdref = ref (Evd.clear_metas sigma) in + let (hyps, concl) = + try Evarutil.clear_hyps_in_evi env evdref sign cl ids + with Evarutil.ClearDependencyError (id, _) -> + errorlabstrm "" (str "Cannot clear " ++ pr_id id) + in + let sigma = !evdref in + let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in + let sigma = Goal.V82.partial_solution_to sigma goal gl ev in + { it = [gl]; sigma } + let get_its_info gls = get_info gls.sigma gls.it let get_strictness,set_strictness = @@ -469,7 +485,7 @@ let thus_tac c ctyp submetas gls = Proofview.V82.of_tactic (exact_check proof) gls else let refiner = concl_refiner list proof gls in - Tactics.refine refiner gls + Tacmach.refine refiner gls (* general forward step *) @@ -1273,7 +1289,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = (fun id -> hrec_for (out_name fix_name) per_info gls1 id) recs in - generalize hrecs gls1 + Proofview.V82.of_tactic (generalize hrecs) gls1 end; match bro with None -> @@ -1349,7 +1365,7 @@ let end_tac et2 gls = (default_justification (List.map mkVar clauses)) | ET_Induction,EK_nodep -> tclTHENLIST - [generalize (pi.per_args@[pi.per_casee]); + [Proofview.V82.of_tactic (generalize (pi.per_args@[pi.per_casee])); Proofview.V82.of_tactic (simple_induct (AnonHyp (succ (List.length pi.per_args)))); default_justification (List.map mkVar clauses)] | ET_Case_analysis,EK_dep tree -> @@ -1361,7 +1377,7 @@ let end_tac et2 gls = (initial_instance_stack clauses) [pi.per_casee] 0 tree | ET_Induction,EK_dep tree -> let nargs = (List.length pi.per_args) in - tclTHEN (generalize (pi.per_args@[pi.per_casee])) + tclTHEN (Proofview.V82.of_tactic (generalize (pi.per_args@[pi.per_casee]))) begin fun gls0 -> let fix_id = @@ -1369,7 +1385,7 @@ let end_tac et2 gls = let c_id = pf_get_new_id (Id.of_string "_main_arg") gls0 in tclTHENLIST - [fix (Some fix_id) (succ nargs); + [Proofview.V82.of_tactic (fix (Some fix_id) (succ nargs)); tclDO nargs (Proofview.V82.of_tactic introf); Proofview.V82.of_tactic (intro_mustbe_force c_id); execute_cases (Name fix_id) pi |