Correction of a bug in Intuition (no more decomposition of dependent pairs).

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

3 files changed, 43 insertions, 6 deletions

diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 0c08da467b..39c2bd8f77 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -121,7 +121,6 @@ let match_with_unit_type t =
 
 let is_unit_type t = op2bool (match_with_unit_type t)
 
-
 (* Checks if a given term is an application of an
    inductive binary relation R, so that R has only one constructor
    establishing its reflexivity.  *)
@@ -154,9 +153,33 @@ let match_with_nottype t =
 
 let is_nottype t = op2bool (match_with_nottype t)
 		     
-let is_imp_term c = match kind_of_term c with
-  | Prod (_,_,b) -> not (dependent (mkRel 1) b)
-  | _              -> false
-
+let is_imp_term c = 
+  match kind_of_term c with
+    | Prod (_,_,b) -> not (dependent (mkRel 1) b)
+    | _              -> false
+
+let rec has_nodep_prod_after n c =
+  match kind_of_term c with
+    | Prod (_,_,b) -> 
+	( n>0 || not (dependent (mkRel 1) b)) 
+	&& (has_nodep_prod_after (n-1) b)
+    | _            -> true
+	  
+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
+        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
+	  
+let is_nodep_ind t=op2bool (match_with_nodep_ind t)
 
 
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 02ba943501..053175269c 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -73,3 +73,16 @@ val is_equation            : testing_function
 
 val match_with_nottype     : (constr * constr) matching_function
 val is_nottype             : testing_function 
+
+
+(* I added these functions to test whether a type contains dependent
+  products or not, and if an inductive has constructors with dependent types
+ (excluding parameters). this is useful to check whether a conjunction is a
+ real conjunction and not a dependent tuple. (Pierre Corbineau, 13/5/2002) *)
+
+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 is_nodep_ind           : testing_function 
+
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index e193b20a97..d971c0c1e0 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -34,7 +34,8 @@ let is_unit ist =
     <:tactic<Fail>>
 
 let is_conj ist =
-  if (is_conjunction (List.assoc 1 ist.lmatch)) then
+  let ind=(List.assoc 1 ist.lmatch) in
+  if (is_conjunction ind) && (is_nodep_ind ind) then
      <:tactic<Idtac>>
   else
     <:tactic<Fail>>