From 47e5f716f7ded0eec43b00d49955d56c370c3596 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 8 Jun 2008 16:13:37 +0000
Subject: - Extension de "generalize" en "generalize c as id at occs". - Ajout
 clause "in" à "remember" (et passage du code en ML). - Ajout clause "in" à
 "induction"/"destruct" qui, en ce cas, ajoute   aussi une égalité pour se
 souvenir du terme sur lequel l'induction   ou l'analyse de cas s'applique. -
 Ajout "pose t as id" en standard (Matthieu: j'ai enlevé celui de   Programs
 qui avait la sémantique de "pose proof" tandis que le nouveau   a la même
 sémantique que "pose (id:=t)"). - Un peu de réorganisation, uniformisation de
 noms dans Arith, et   ajout EqNat dans Arith. - Documentation tactiques et
 notations de tactiques.

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

(limited to 'proofs')

diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 34699c5fdd..d0b0155529 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -27,6 +27,7 @@ type rec_flag = bool       (* true = recursive        false = not recursive *)
 type advanced_flag = bool  (* true = advanced         false = basic *)
 type split_flag = bool     (* true = exists           false = split *)
 type hidden_flag = bool    (* true = internal use     false = user-level *)
+type letin_flag = bool     (* true = use local def    false = use Leibniz *)
 
 type raw_red_flag =
   | FBeta
@@ -147,17 +148,17 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacMutualCofix of hidden_flag * identifier * (identifier * 'constr) list
   | TacCut of 'constr
   | TacAssert of 'tac option * intro_pattern_expr * 'constr
-  | TacGeneralize of 'constr list
+  | TacGeneralize of ('constr with_occurrences * name) list
   | TacGeneralizeDep of 'constr
-  | TacLetTac of name * 'constr * 'id gclause
+  | TacLetTac of name * 'constr * 'id gclause * letin_flag
 
   (* Derived basic tactics *)
   | TacSimpleInduction of quantified_hypothesis
   | TacNewInduction of evars_flag * 'constr with_bindings induction_arg list * 
-      'constr with_bindings option * intro_pattern_expr
+      'constr with_bindings option * intro_pattern_expr * 'id gclause option
   | TacSimpleDestruct of quantified_hypothesis
   | TacNewDestruct of evars_flag * 'constr with_bindings induction_arg list *
-      'constr with_bindings option * intro_pattern_expr
+      'constr with_bindings option * intro_pattern_expr * 'id gclause option
 
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
   | TacDecomposeAnd of 'constr
-- 
cgit v1.2.3