diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-16 18:34:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-16 21:17:25 +0200 |
| commit | 12f4c8ed277fa8368cab2e99f173339a64bcef3d (patch) | |
| tree | e6a5072d1f747d0266fe7d6af9ef666b39f3dcce /plugins | |
| parent | dc8750d166cffd846619d2de20e02a4e31c6357f (diff) | |
Put the "fix" tactic in the monad.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 8 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
3 files changed, 6 insertions, 6 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 4f2270313..a6b338164 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1385,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 diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index fdb112ba0..0b7a1e646 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1227,10 +1227,10 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam if this_fix_info.idx + 1 = 0 then tclIDTAC (* Someone tries to defined a principle on a fully parametric definition declared as a fixpoint (strange but ....) *) else - observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (fix (Some this_fix_info.name) (this_fix_info.idx +1)) + observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (Proofview.V82.of_tactic (fix (Some this_fix_info.name) (this_fix_info.idx +1))) else - Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1) - other_fix_infos 0 + Proofview.V82.of_tactic (Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1) + other_fix_infos 0) | _ -> anomaly (Pp.str "Not a valid information") in let first_tac : tactic = (* every operations until fix creations *) @@ -1642,7 +1642,7 @@ let prove_principle_for_gen (* observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids))); (* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++ *) (* str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *) - (* observe_tac "h_fix " *) (fix (Some fix_id) (List.length args_ids + 1)); + (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix (Some fix_id) (List.length args_ids + 1))); (* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *) h_intros (List.rev (acc_rec_arg_id::args_ids)); Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref)); diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index ac81366bb..c1c3801b4 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1119,7 +1119,7 @@ let termination_proof_header is_mes input_type ids args_id relation tclTHEN (Tactics.generalize [mkVar id]) (Proofview.V82.of_tactic (clear [id]))) )) ; - observe_tac (str "fix") (fix (Some hrec) (nargs+1)); + observe_tac (str "fix") (Proofview.V82.of_tactic (fix (Some hrec) (nargs+1))); h_intros args_id; Proofview.V82.of_tactic (Simple.intro wf_rec_arg); observe_tac (str "tac") (tac wf_rec_arg hrec wf_rec_arg acc_inv) |