From 58529cf2252bf6ae386a45c8587bdc9b3285c1c5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 16 Jan 2006 13:59:08 +0000
Subject: Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq
 choisir un nom; utilisation de IntroAnonymous au lieu de None dans l'argument
 "with_names" des tactiques induction, inversion et assert.

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

(limited to 'proofs')

diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index c2b226281c..8f27088f0d 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -69,8 +69,8 @@ type inversion_kind =
   | FullInversionClear
 
 type ('c,'id) inversion_strength =
-  | NonDepInversion of inversion_kind * 'id list * intro_pattern_expr option
-  | DepInversion of inversion_kind * 'c option * intro_pattern_expr option
+  | NonDepInversion of inversion_kind * 'id list * intro_pattern_expr
+  | DepInversion of inversion_kind * 'c option * intro_pattern_expr
   | InversionUsing of 'c * 'id list
 
 type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
@@ -125,7 +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
-  | TacAssert of 'tac option * intro_pattern_expr option * 'constr
+  | TacAssert of 'tac option * intro_pattern_expr * 'constr
   | TacGeneralize of 'constr list
   | TacGeneralizeDep of 'constr
   | TacLetTac of name * 'constr * 'id gclause
@@ -134,10 +134,10 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   (* Derived basic tactics *)
   | TacSimpleInduction of quantified_hypothesis
   | TacNewInduction of 'constr induction_arg * 'constr with_bindings option
-      * intro_pattern_expr option
+      * intro_pattern_expr
   | TacSimpleDestruct of quantified_hypothesis
   | TacNewDestruct of 'constr induction_arg * 'constr with_bindings option
-      * intro_pattern_expr option
+      * intro_pattern_expr
 
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
   | TacDecomposeAnd of 'constr
-- 
cgit v1.2.3