From 32716cc80cbda47e59e26c920ffb0ab738b0e9c0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 27 Apr 2016 22:13:04 +0200
Subject: Revert "In the short term, stronger invariant on the syntax of
 TacAssert, what"

This reverts commit bde36d4b00185065628324d8ca71994f84eae244.
---
 tactics/tactics.ml  | 7 ++-----
 tactics/tactics.mli | 2 +-
 2 files changed, 3 insertions(+), 6 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4c47dc67e3..a626092dd1 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2551,9 +2551,6 @@ let forward b usetac ipat c =
 	(Proofview.V82.tactic (exact_no_check c))
       end }
   | Some tac ->
-      let tac = match tac with
-        | None -> Tacticals.New.tclIDTAC
-        | Some tac -> Tacticals.New.tclCOMPLETE tac in
       if b then
         Tacticals.New.tclTHENFIRST (assert_as b None ipat c) tac
       else
@@ -2561,8 +2558,8 @@ let forward b usetac ipat c =
           (assert_as b None ipat c) [||] tac [|Tacticals.New.tclIDTAC|]
 
 let pose_proof na c = forward true None (ipat_of_name na) c
-let assert_by na t tac = forward true (Some (Some tac)) (ipat_of_name na) t
-let enough_by na t tac = forward false (Some (Some tac)) (ipat_of_name na) t
+let assert_by na t tac = forward true (Some tac) (ipat_of_name na) t
+let enough_by na t tac = forward false (Some tac) (ipat_of_name na) t
 
 (***************************)
 (*  Generalization tactics *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 0919fb28e2..4c4a96ec07 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -365,7 +365,7 @@ val pose_proof : Name.t -> constr ->
 
 (** Common entry point for user-level "assert", "enough" and "pose proof" *)
 
-val forward   : bool -> unit Proofview.tactic option option ->
+val forward   : bool -> unit Proofview.tactic option ->
   intro_pattern option -> constr -> unit Proofview.tactic
 
 (** Implements the tactic cut, actually a modus ponens rule *)
-- 
cgit v1.2.3