From b47ef72ac6e2498a5dcd5e71279d2feddfa0c9c9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 10 Oct 2003 18:56:41 +0000
Subject: Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4575 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/inv.mli | 29 +++++++++++++++++------------
 1 file changed, 17 insertions(+), 12 deletions(-)

diff --git a/tactics/inv.mli b/tactics/inv.mli
index 9375efdea2..c310f75279 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -12,27 +12,32 @@
 open Names
 open Term
 open Tacmach
+open Tacexpr
+open Rawterm
 (*i*)
 
 type inversion_status = Dep of constr option | NoDep
 
 val inv_gen :
-  bool -> bool option -> inversion_status -> Rawterm.quantified_hypothesis -> tactic
-val invIn_gen : bool option -> Rawterm.quantified_hypothesis -> identifier list -> tactic
+  bool -> inversion_kind -> inversion_status ->
+    case_intro_pattern_expr -> quantified_hypothesis -> tactic
+val invIn_gen :
+  inversion_kind -> case_intro_pattern_expr -> identifier list -> 
+    quantified_hypothesis -> tactic
+
+val inv_clause :
+  inversion_kind -> case_intro_pattern_expr -> identifier list ->
+    quantified_hypothesis -> tactic
+
+val inv : inversion_kind -> case_intro_pattern_expr ->
+  quantified_hypothesis -> tactic
+
+val dinv : inversion_kind -> constr option -> case_intro_pattern_expr ->
+  quantified_hypothesis -> tactic
 
-val inv : bool option -> Rawterm.quantified_hypothesis -> tactic
-val dinv : bool option -> constr option -> Rawterm.quantified_hypothesis -> tactic
 val half_inv_tac : identifier -> tactic
 val inv_tac : identifier -> tactic
 val inv_clear_tac : identifier -> tactic
 val half_dinv_tac : identifier -> tactic
 val dinv_tac : identifier -> tactic
 val dinv_clear_tac : identifier -> tactic
-(*
-val half_dinv_with : identifier -> constr -> tactic
-val dinv_with : identifier -> constr -> tactic
-val dinv_clear_with : identifier -> constr -> tactic
-*)
-(*
-val invIn_tac : identifier -> identifier -> identifier list -> tactic
-*)
-- 
cgit v1.2.3