diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-12 22:25:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-16 17:30:18 +0200 |
| commit | e2d4490b12514362af8e1f0b8b89cf0550f78130 (patch) | |
| tree | ddb275621606524ccd6af7b5a9b94b36988041c0 /tactics | |
| parent | 613d99b98d3c78213a69acdbf23c660764487300 (diff) | |
A stronger invariant on the syntax of TacAssert, what allows for a
simpler re-printing of assert.
Also fixing the precedence for printing "by" clause.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 7 | ||||
| -rw-r--r-- | tactics/tactics.mli | 2 |
2 files changed, 6 insertions, 3 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 991922d90..2f24e55a5 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2676,6 +2676,9 @@ let forward b usetac ipat c = Tacticals.New.tclTHENFIRST (assert_as true hd ipat t) (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 @@ -2683,8 +2686,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 tac) (ipat_of_name na) t -let enough_by na t tac = forward false (Some tac) (ipat_of_name na) t +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 (***************************) (* Generalization tactics *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index fa7b6791e..142fdd3eb 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -366,7 +366,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 -> +val forward : bool -> unit Proofview.tactic option option -> intro_pattern option -> constr -> unit Proofview.tactic (** Implements the tactic cut, actually a modus ponens rule *) |