diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 22:13:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 22:13:04 +0200 |
| commit | 32716cc80cbda47e59e26c920ffb0ab738b0e9c0 (patch) | |
| tree | aa30dbcd367b5079f6308f9d9fad0c62b70bc964 /tactics/tactics.ml | |
| parent | cc3f28467f826506b8eb6e07c3b2db9ffd2ed3ba (diff) | |
Revert "In the short term, stronger invariant on the syntax of TacAssert, what"
This reverts commit bde36d4b00185065628324d8ca71994f84eae244.
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 4c47dc67e..a626092dd 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 *) |