Ground Update.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4188 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 25 insertions, 13 deletions

diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 6c4a01f262..2748ab4678 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -209,17 +209,19 @@ let has_nodep_prod = has_nodep_prod_after 0
 	
 let match_with_nodep_ind t =
   let (hdapp,args) = decompose_app t in
-  match (kind_of_term hdapp) with
-    | Ind ind  -> 
-        let (mib,mip) = Global.lookup_inductive ind in
-          if mip.mind_nrealargs>0 then None else
-	    let constr_types = mip.mind_nf_lc in 
-	    let nodep_constr = has_nodep_prod_after mip.mind_nparams in	
-	      if array_for_all nodep_constr constr_types then 
-		Some (hdapp,args)
-              else 
-		None
-    | _ -> None
+    match (kind_of_term hdapp) with
+      | Ind ind  -> 
+          let (mib,mip) = Global.lookup_inductive ind in
+	    if Array.length (mib.mind_packets)>1 then None else
+	      let nodep_constr = has_nodep_prod_after mip.mind_nparams in
+		if array_for_all nodep_constr mip.mind_nf_lc then
+		  let params=
+		    if mip.mind_nrealargs=0 then args else
+		      fst (list_chop mip.mind_nparams args) in
+		    Some (hdapp,params,mip.mind_nrealargs)
+		else 
+		  None
+      | _ -> None
 	  
 let is_nodep_ind t=op2bool (match_with_nodep_ind t)
 
@@ -228,7 +230,8 @@ let match_with_sigma_type t=
   match (kind_of_term hdapp) with
     | Ind ind  -> 
         let (mib,mip) = Global.lookup_inductive ind in
-          if (mip.mind_nrealargs=0) &&
+          if (Array.length (mib.mind_packets)=1) &&
+	    (mip.mind_nrealargs=0) &&
 	    (Array.length mip.mind_consnames=1) &&
 	    has_nodep_prod_after (mip.mind_nparams+1) mip.mind_nf_lc.(0) then
 	      (*allowing only 1 existential*) 
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 3dd6a420f4..b70d3f21a4 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -88,7 +88,7 @@ val is_imp_term            : testing_function
 val has_nodep_prod_after   : int -> testing_function
 val has_nodep_prod         : testing_function
 
-val match_with_nodep_ind   : (constr * constr list) matching_function	  
+val match_with_nodep_ind   : (constr * constr list * int) matching_function  
 val is_nodep_ind           : testing_function 
 
 val match_with_sigma_type   : (constr * constr list) matching_function	  
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 6978efdbae..475b29be4c 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -63,6 +63,9 @@ let tclPROGRESS      = Refiner.tclPROGRESS
 let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS
 let tclNOTSAMEGOAL   = Refiner.tclNOTSAMEGOAL
 let tclTHENTRY       = tclTHENTRY
+let tclIFTHENELSE    = tclIFTHENELSE
+let tclIFTHENSELSE   = tclIFTHENSELSE
+let tclIFTHENSVELSE   = tclIFTHENSVELSE
 
 let unTAC            = unTAC
 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 3a42dc227e..4a1e034755 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -57,6 +57,12 @@ val tclLAST_HYP      : (constr -> tactic) -> tactic
 val tclTRY_sign      : (constr -> tactic) -> named_context -> tactic
 val tclTRY_HYPS      : (constr -> tactic) -> tactic
 
+val tclIFTHENELSE    : tactic -> tactic -> tactic -> tactic
+val tclIFTHENSELSE   : tactic -> tactic list -> tactic -> tactic
+val tclIFTHENSVELSE  : tactic -> tactic array -> tactic -> tactic
+
+
+
 val unTAC            : tactic -> goal sigma -> proof_tree sigma
 
 (*s Clause tacticals. *)