From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Fri, 8 Aug 2008 13:18:42 +0200
Subject: Imported Upstream version 8.2~beta4+dfsg

---
 tactics/tacticals.mli | 24 ++++++++++++++++--------
 1 file changed, 16 insertions(+), 8 deletions(-)

(limited to 'tactics/tacticals.mli')

diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index e97abe9f..6826977b 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -6,10 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tacticals.mli 10785 2008-04-13 21:41:54Z herbelin $ i*)
+(*i $Id: tacticals.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
 
 (*i*)
 open Pp
+open Util
 open Names
 open Term
 open Sign
@@ -124,23 +125,30 @@ type branch_args = {
   nassums    : int;         (* the number of assumptions to be introduced *)
   branchsign : bool list;   (* the signature of the branch.
                                true=recursive argument, false=constant *)
-  branchnames : intro_pattern_expr list}
+  branchnames : intro_pattern_expr located list}
 
 type branch_assumptions = {
   ba        : branch_args;     (* the branch args *)
   assums    : named_context}   (* the list of assumptions introduced *)
 
+(* [check_disjunctive_pattern_size loc pats n] returns an appropriate *)
+(* error message if |pats| <> n *)
+val check_or_and_pattern_size :
+  Util.loc -> or_and_intro_pattern_expr -> int -> unit 
+
 (* Useful for [as intro_pattern] modifier *)
 val compute_induction_names : 
-  int -> intro_pattern_expr -> intro_pattern_expr list array
+  int -> intro_pattern_expr located option -> 
+    intro_pattern_expr located list array
 
 val elimination_sort_of_goal : goal sigma -> sorts_family
 val elimination_sort_of_hyp  : identifier -> goal sigma -> sorts_family
 
 val general_elim_then_using :
-  (inductive -> goal sigma -> constr) -> rec_flag -> intro_pattern_expr ->
-    (branch_args -> tactic) -> constr option -> 
-      (arg_bindings * arg_bindings) -> inductive -> clausenv -> tactic
+  (inductive -> goal sigma -> constr) -> rec_flag ->
+  intro_pattern_expr located option -> (branch_args -> tactic) -> 
+    constr option -> (arg_bindings * arg_bindings) -> inductive -> clausenv ->
+    tactic
 	  
 val elimination_then_using :
   (branch_args -> tactic) -> constr option -> 
@@ -151,12 +159,12 @@ val elimination_then :
     (arg_bindings * arg_bindings) -> constr -> tactic
 
 val case_then_using :
-  intro_pattern_expr -> (branch_args -> tactic) -> 
+  intro_pattern_expr located option -> (branch_args -> tactic) -> 
     constr option -> (arg_bindings * arg_bindings) ->
       inductive -> clausenv -> tactic
 
 val case_nodep_then_using :
-  intro_pattern_expr -> (branch_args -> tactic) -> 
+  intro_pattern_expr located option -> (branch_args -> tactic) -> 
     constr option -> (arg_bindings * arg_bindings) -> 
       inductive -> clausenv -> tactic
 
-- 
cgit v1.2.3