From 44510966ab7240c60f28f4f2e99d382e155b084b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 16 Jan 2006 09:55:24 +0000
Subject: - Tactic "assert" now accepts "as" intro patterns and "by" tactic
 clauses - New tactic "pose proof" that generalizes "assert (id:=p)" with
 intro patterns - TacTrueCut and TacForward merged into new TacAssert bound to
 Tactics.forward

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7875 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tacexpr.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index b8de1e789a..c2b226281c 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -84,6 +84,8 @@ type 'id gclause =
     onconcl : bool;
     concl_occs :int list }
 
+let nowhere = {onhyps=Some[]; onconcl=false; concl_occs=[]}
+
 let simple_clause_of = function
     { onhyps = Some[scl]; onconcl = false } -> Some scl
   | { onhyps = Some []; onconcl = true; concl_occs=[] } -> None
@@ -123,8 +125,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacCofix of identifier option
   | TacMutualCofix of identifier * (identifier * 'constr) list
   | TacCut of 'constr
-  | TacTrueCut of name * 'constr 
-  | TacForward of bool * name * 'constr
+  | TacAssert of 'tac option * intro_pattern_expr option * 'constr
   | TacGeneralize of 'constr list
   | TacGeneralizeDep of 'constr
   | TacLetTac of name * 'constr * 'id gclause
-- 
cgit v1.2.3