diff options
Diffstat (limited to 'plugins')
-rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 4 | ||||
-rw-r--r-- | plugins/funind/recdef.ml | 2 | ||||
-rw-r--r-- | plugins/ltac/coretactics.ml4 | 6 |
3 files changed, 5 insertions, 7 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index ccf109ce1..5e0d3e8ee 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1242,7 +1242,7 @@ 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) ) (Proofview.V82.of_tactic (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 this_fix_info.name (this_fix_info.idx +1))) else Proofview.V82.of_tactic (Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1) other_fix_infos 0) @@ -1657,7 +1657,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 " *) (Proofview.V82.of_tactic (fix (Some fix_id) (List.length args_ids + 1))); + (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix 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 45c9eff2f..ab03f1831 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1152,7 +1152,7 @@ let termination_proof_header is_mes input_type ids args_id relation tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (Proofview.V82.of_tactic (clear [id]))) )) ; - observe_tac (str "fix") (Proofview.V82.of_tactic (fix (Some hrec) (nargs+1))); + observe_tac (str "fix") (Proofview.V82.of_tactic (fix 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) diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 931633e1a..faa9e413b 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -273,15 +273,13 @@ END (* Fix *) TACTIC EXTEND fix - [ "fix" natural(n) ] -> [ Tactics.fix None n ] -| [ "fix" ident(id) natural(n) ] -> [ Tactics.fix (Some id) n ] + [ "fix" ident(id) natural(n) ] -> [ Tactics.fix id n ] END (* Cofix *) TACTIC EXTEND cofix - [ "cofix" ] -> [ Tactics.cofix None ] -| [ "cofix" ident(id) ] -> [ Tactics.cofix (Some id) ] + [ "cofix" ident(id) ] -> [ Tactics.cofix id ] END (* Clear *) |