From 12f4c8ed277fa8368cab2e99f173339a64bcef3d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 May 2016 18:34:21 +0200 Subject: Put the "fix" tactic in the monad. --- plugins/funind/recdef.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind/recdef.ml') 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) -- cgit v1.2.3