- Another bug in get_sort_family_of (sort-polymorphism of constants and

  inductive types was not taken into account).
- Virtually extended tauto to 
  - support arbitrary-length disjunctions and conjunctions,
  - support arbitrary complex forms of disjunctions and
    conjunctions when in the contravariant of an implicative hypothesis,
  - stick with the purely propositional fragment and not apply reflexivity.
  This is virtual in the sense that it is not activated since it breaks 
  compatibility with the existing tauto.
- Modified the notion of conjunction and unit type used in hipattern in a 
  way that is closer to the intuitive meaning (forbid dependencies 
  between parameters in conjunction; forbid indices in unit types).
- Investigated how far "iff" could be turned into a direct inductive
  definition; modified tauto.ml4 so that it works with the current and
  the alternative definition.
- Fixed a bug in the error message from lookup_eliminator.
- Other minor changes.



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

8 files changed, 240 insertions, 153 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index b1e6693889..0dd90246db 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -279,7 +279,7 @@ let make_exact_entry pri (c,cty) =
         let ce = mk_clenv_from dummy_goal (c,cty) in
 	let c' = clenv_type ce in
 	let pat = Pattern.pattern_of_constr c' in
-	(Some (head_of_constr_reference (List.hd (head_constr cty))),
+	(Some (head_of_constr_reference (fst (head_constr cty))),
 	   { pri=(match pri with Some pri -> pri | None -> 0); pat=Some pat; code=Give_exact c })
 
 let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) =
@@ -352,7 +352,7 @@ let make_extern pri pat tacast =
 
 let make_trivial env sigma c =
   let t = hnf_constr env sigma (type_of env sigma c) in
-  let hd = head_of_constr_reference (List.hd (head_constr t)) in
+  let hd = head_of_constr_reference (fst (head_constr t)) in
   let ce = mk_clenv_from dummy_goal (c,t) in
   (Some hd, { pri=1;
          pat = Some (Pattern.pattern_of_constr (clenv_type ce));
@@ -412,8 +412,8 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) =
   let subst_key gr =
     let (lab'', elab') = subst_global subst gr in
     let gr' = 
-      (try head_of_constr_reference (List.hd (head_constr_bound elab' []))
-	with Tactics.Bound -> lab'')
+      (try head_of_constr_reference (fst (head_constr_bound elab'))
+       with Tactics.Bound -> lab'')
     in if gr' == gr then gr else gr'
   in
   let subst_hint (k,data as hint) =
@@ -637,10 +637,7 @@ let print_hint_ref ref =  ppnl(pr_hint_ref ref)
 
 let pr_hint_term cl = 
   try 
-    let (hdc,args) = match head_constr_bound cl [] with 
-      | hdc::args -> (hdc,args)
-      | [] -> assert false 
-    in
+    let (hdc,args) = head_constr_bound cl in
     let hd = head_of_constr_reference hdc in
     let dbs = Hintdbmap.to_list !searchtable in
     let valid_dbs = 
@@ -864,7 +861,7 @@ and tac_of_hint db_list local_db concl (flags, {pat=p; code=t}) =
       
 and trivial_resolve mod_delta db_list local_db cl = 
   try 
-    let hdconstr = List.hd (head_constr_bound cl []) in
+    let hdconstr,_ = head_constr_bound cl in
     List.map (tac_of_hint db_list local_db cl)
       (priority 
 	(my_find_search mod_delta db_list local_db
@@ -906,7 +903,7 @@ let h_trivial lems l =
 
 let possible_resolve mod_delta db_list local_db cl =
   try 
-    let hdconstr = List.hd (head_constr_bound cl []) in
+    let hdconstr,_ = head_constr_bound cl in
     List.map (tac_of_hint db_list local_db cl)
       (my_find_search mod_delta db_list local_db
         (head_of_constr_reference hdconstr) cl)
@@ -915,15 +912,16 @@ let possible_resolve mod_delta db_list local_db cl =
 
 let decomp_unary_term_then (id,_,typc) kont1 kont2 gl =
   try
-    let hd = List.hd (head_constr typc) in 
-    match Hipattern.match_with_conjunction_size hd with
-    | Some (_,_,n) -> tclTHEN (simplest_case (mkVar id)) (kont1 n) gl
-    | None -> kont2 gl
+    let ccl = applist (head_constr typc) in
+    match Hipattern.match_with_conjunction ccl with
+    | Some (_,args) ->
+	tclTHEN (simplest_case (mkVar id)) (kont1 (List.length args)) gl
+    | None ->
+	kont2 gl
   with UserError _ -> kont2 gl
 
 let decomp_empty_term (id,_,typc) gl = 
-  let (hd,_) = decompose_app typc in 
-  if Hipattern.is_empty_type hd then 
+  if Hipattern.is_empty_type typc then 
     simplest_case (mkVar id) gl 
   else 
     errorlabstrm "Auto.decomp_empty_term" (str "Not an empty type.")
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 3471289216..b556676ee6 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -146,13 +146,13 @@ and e_my_find_search db_list local_db hdc concl =
 and e_trivial_resolve db_list local_db gl = 
   try 
     e_my_find_search db_list local_db 
-      (List.hd (head_constr_bound gl [])) gl
+      (fst (head_constr_bound gl)) gl
   with Bound | Not_found -> []
 
 let e_possible_resolve db_list local_db gl =
   try 
     e_my_find_search db_list local_db 
-      (List.hd (head_constr_bound gl [])) gl
+      (fst (head_constr_bound gl)) gl
   with Bound | Not_found -> []
 
 let find_first_goal gls = 
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index dd51acc7b8..5e4f847fa8 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -198,13 +198,13 @@ and e_trivial_resolve mod_delta db_list local_db gl =
   try 
     priority 
       (e_my_find_search mod_delta db_list local_db 
-	 (List.hd (head_constr_bound gl [])) gl)
+	 (fst (head_constr_bound gl)) gl)
   with Bound | Not_found -> []
 
 let e_possible_resolve mod_delta db_list local_db gl =
   try List.map snd 
     (e_my_find_search mod_delta db_list local_db 
-	(List.hd (head_constr_bound gl [])) gl)
+	(fst (head_constr_bound gl)) gl)
   with Bound | Not_found -> []
 
 let assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id))
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index c796eda905..7696811551 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -15,6 +15,7 @@ open Util
 open Names
 open Nameops
 open Term
+open Sign
 open Termops
 open Reductionops
 open Inductiveops
@@ -64,48 +65,83 @@ let match_with_non_recursive_type t =
 
 let is_non_recursive_type t = op2bool (match_with_non_recursive_type t)
 
-(* A general conjunction type is a non-recursive inductive type with
-   only one constructor. *)
+(* Test dependencies *)
 
-let match_with_conjunction_size 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 (Array.length mip.mind_consnames = 1)
-	  && (not (mis_is_recursive (ind,mib,mip)))
-          && (mip.mind_nrealargs = 0)
-        then 
-	  Some (hdapp,args,mip.mind_consnrealdecls.(0))
-        else 
-	  None
-    | _ -> None
-
-let match_with_conjunction t =
-  match match_with_conjunction_size t with
-  | Some (hd,args,n) -> Some (hd,args)
-  | None -> None
+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 is_conjunction t = op2bool (match_with_conjunction t)
-    
-(* A general disjunction type is a non-recursive inductive type all
-   whose constructors have a single argument. *)
+(* A general conjunctive type is a non-recursive with-no-indices inductive 
+   type with only one constructor and no dependencies between argument;
+   it is strict if it has the form 
+   "Inductive I A1 ... An := C (_:A1) ... (_:An)" *)
 
-let match_with_disjunction t =
+let match_with_conjunction ?(strict=false) t =
   let (hdapp,args) = decompose_app t in 
   match kind_of_term hdapp with
-    | Ind ind  ->
-        let car = mis_constr_nargs ind in
-	if array_for_all (fun ar -> ar = 1) car &&
-	   (let (mib,mip) = Global.lookup_inductive ind in
-            not (mis_is_recursive (ind,mib,mip)))
-        then 
+  | Ind ind -> 
+      let (mib,mip) = Global.lookup_inductive ind in
+      if (Array.length mip.mind_consnames = 1)
+	&& (not (mis_is_recursive (ind,mib,mip)))
+        && (mip.mind_nrealargs = 0)
+      then
+	let is_nth_argument n (_,b,c) = b=None && c=mkRel(n+mib.mind_nparams) in
+	if strict &&
+	  list_for_all_i is_nth_argument 1 
+	    (fst (decompose_prod_n_assum mib.mind_nparams mip.mind_nf_lc.(0)))
+	then
 	  Some (hdapp,args)
-        else 
-	  None
-    | _ -> None
+	else
+	  let ctyp = prod_applist mip.mind_nf_lc.(0) args in
+	  let cargs = List.map pi3 (fst (decompose_prod_assum ctyp)) in
+	  if has_nodep_prod ctyp then
+	    Some (hdapp,List.rev cargs)
+	  else None
+      else None
+  | _ -> None
+
+let is_conjunction ?(strict=false) t =
+  op2bool (match_with_conjunction ~strict t)
+
+(* A general disjunction type is a non-recursive with-no-indices inductive 
+   type with of which all constructors have a single argument;
+   it is strict if it has the form 
+   "Inductive I A1 ... An := C1 (_:A1) | ... | Cn : (_:An)" *)
+
+let match_with_disjunction ?(strict=false) t =
+  let (hdapp,args) = decompose_app t in 
+  match kind_of_term hdapp with
+  | Ind ind  ->
+      let car = mis_constr_nargs ind in
+      let (mib,mip) = Global.lookup_inductive ind in
+      if array_for_all (fun ar -> ar = 1) car &&
+	not (mis_is_recursive (ind,mib,mip))
+      then
+	if strict &
+	  array_for_all_i (fun i c -> 
+	    snd (decompose_prod_n_assum mib.mind_nparams c) = mkRel i) 1
+	  mip.mind_nf_lc
+	then
+	  Some (hdapp,args)
+	else
+	  let cargs =
+	    Array.map (fun ar -> pi2 (destProd (prod_applist ar args)))
+	      mip.mind_nf_lc in
+	  Some (hdapp,Array.to_list cargs)
+      else 
+	None
+  | _ -> None
 
-let is_disjunction t = op2bool (match_with_disjunction t)
+let is_disjunction ?(strict=false) t =
+  op2bool (match_with_disjunction ~strict t)
+
+(* An empty type is an inductive type, possible with indices, that has no
+   constructors *)
 
 let match_with_empty_type t =
   let (hdapp,args) = decompose_app t in
@@ -118,22 +154,32 @@ let match_with_empty_type t =
 	  
 let is_empty_type t = op2bool (match_with_empty_type t)
 
-let match_with_unit_type t =
+(* This filters inductive types with one constructor with no arguments;
+   Parameters and indices are allowed *)
+
+let match_with_unit_or_eq_type 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 nconstr = Array.length mip.mind_consnames in
-        let zero_args c =
-	  nb_prod c = mib.mind_nparams in  
+        let zero_args c = nb_prod c = mib.mind_nparams in  
 	if nconstr = 1 && zero_args constr_types.(0) then 
 	  Some hdapp
-        else 
+	else 
 	  None
     | _ -> None
 
-let is_unit_type t = op2bool (match_with_unit_type t)
+let is_unit_or_eq_type t = op2bool (match_with_unit_or_eq_type t)
+
+(* A unit type is an inductive type with no indices but possibly
+   (useless) parameters, and that has no constructors *)
+
+let is_unit_type t =
+  match match_with_conjunction t with
+  | Some (_,t) when List.length t = 0 -> true
+  | _ -> false
 
 (* Checks if a given term is an application of an
    inductive binary relation R, so that R has only one constructor
@@ -204,15 +250,6 @@ let match_with_imp_term c=
 
 let is_imp_term c = op2bool (match_with_imp_term c) 
 
-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
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index a97891c14c..b2e25b42d2 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -52,19 +52,20 @@ type testing_function = constr -> bool
 val match_with_non_recursive_type : (constr * constr list) matching_function
 val is_non_recursive_type         : testing_function 
 
-val match_with_disjunction : (constr * constr list) matching_function
-val is_disjunction         : testing_function 
+val match_with_disjunction : ?strict:bool -> (constr * constr list) matching_function
+val is_disjunction         : ?strict:bool -> testing_function 
 
-val match_with_conjunction : (constr * constr list) matching_function
-val match_with_conjunction_size : (constr * constr list * int) matching_function
-val is_conjunction         : testing_function 
+val match_with_conjunction : ?strict:bool -> (constr * constr list) matching_function
+val is_conjunction         : ?strict:bool -> testing_function 
 
 val match_with_empty_type  : constr matching_function
 val is_empty_type          : testing_function 
 
-val match_with_unit_type   : constr matching_function
+(* type with only one constructor and no arguments, possibly with indices *)
+val match_with_unit_or_eq_type : constr matching_function
+val is_unit_or_eq_type     : testing_function 
 
-(* type with only one constructor and no arguments *)
+(* type with only one constructor and no arguments, no indices *)
 val is_unit_type           : testing_function 
 
 val match_with_equation    : (constr * constr list) matching_function
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6f06c25a0b..c43f829fd0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -85,15 +85,6 @@ let dloc = dummy_loc
 (* General functions                    *)
 (****************************************)
 
-(*
-let get_pairs_from_bindings = 
-  let pair_from_binding = function  
-    | [(Bindings binds)] -> binds
-    | _                  -> error "not a binding list!"
-  in 
-  List.map pair_from_binding
-*)
-
 let string_of_inductive c = 
   try match kind_of_term c with
   | Ind ind_sp -> 
@@ -102,26 +93,16 @@ let string_of_inductive c =
   | _ -> raise Bound
   with Bound -> error "Bound head variable."
 
-let rec head_constr_bound t l =
-  let t = strip_outer_cast(collapse_appl t) in
-  match kind_of_term t with
-    | Prod (_,_,c2)  -> head_constr_bound c2 l 
-    | LetIn (_,_,_,c2) -> head_constr_bound c2 l 
-    | App (f,args)  -> 
-	head_constr_bound f (Array.fold_right (fun a l -> a::l) args l)
-    | Const _        -> t::l
-    | Ind _       -> t::l
-    | Construct _ -> t::l
-    | Var _          -> t::l
-    | _                -> raise Bound
+let rec head_constr_bound t =
+  let t = strip_outer_cast t in
+  let _,ccl = decompose_prod_assum t in
+  let hd,args = decompose_app ccl in
+  match kind_of_term hd with
+    | Const _ | Ind _ | Construct _ | Var _ -> (hd,args)
+    | _ -> raise Bound
 
 let head_constr c = 
-  try head_constr_bound c [] with Bound -> error "Bound head variable."
-
-(*
-let bad_tactic_args s l =
-  raise (RefinerError (BadTacticArgs (s,l)))
-*)
+  try head_constr_bound c with Bound -> error "Bound head variable."
 
 (******************************************)
 (*           Primitive tactics            *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 01d517c163..8765541b29 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -39,8 +39,8 @@ val inj_ebindings : constr bindings -> open_constr bindings
 (*s General functions. *)
 
 val string_of_inductive : constr -> string
-val head_constr       : constr -> constr list
-val head_constr_bound : constr -> constr list -> constr list
+val head_constr       : constr -> constr * constr list
+val head_constr_bound : constr -> constr * constr list
 val is_quantified_hypothesis : identifier -> goal sigma -> bool
 
 exception Bound
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index d3dd2959c3..3d85f65608 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -21,19 +21,44 @@ open Tacinterp
 open Tactics
 open Util
 
-let assoc_last ist =
-  match List.assoc (Names.id_of_string "X1") ist.lfun with
+let assoc_var s ist =
+  match List.assoc (Names.id_of_string s) ist.lfun with
     | VConstr c -> c
     | _ -> failwith "tauto: anomaly"
 
+(** Parametrization of tauto *)
+
+(* Whether conjunction and disjunction are restricted to binary connectives *)
+(* (this is the compatibility mode) *)
+let binary_mode = true
+
+(* Whether conjunction and disjunction are restricted to the connectives *)
+(* having the structure of "and" and "or" (up to the choice of sorts) in *)
+(* contravariant position in an hypothesis (this is the compatibility mode) *)
+let strict_in_contravariant_hyp = true
+
+(* Whether conjunction and disjunction are restricted to the connectives *)
+(* having the structure of "and" and "or" (up to the choice of sorts) in *)
+(* an hypothesis and in the conclusion *)
+let strict_in_hyp_and_ccl = false
+
+(* Whether unit type includes equality types *)
+let strict_unit = false
+
+
+(** Test *)
+
 let is_empty ist =
-  if is_empty_type (assoc_last ist) then
+  if is_empty_type (assoc_var "X1" ist) then
     <:tactic<idtac>>
   else
     <:tactic<fail>>
 
-let is_unit ist =
-  if is_unit_type (assoc_last ist) then
+(* Strictly speaking, this exceeds the propositional fragment as it
+   matches also equality types (and solves them if a reflexivity) *)
+let is_unit_or_eq ist =
+  let test = if strict_unit then is_unit_type else is_unit_or_eq_type in
+  if test (assoc_var "X1" ist) then
     <:tactic<idtac>>
   else
     <:tactic<fail>>
@@ -47,93 +72,138 @@ let is_record t =
       | _ -> false
 
 let is_binary t =
+  isApp t &&
   let (hdapp,args) = decompose_app t in
     match (kind_of_term hdapp) with
     | Ind ind  -> 
         let (mib,mip) = Global.lookup_inductive ind in
 	  mib.Declarations.mind_nparams = 2
     | _ -> false
-	
+
+let iter_tac tacl =
+  List.fold_right (fun tac tacs -> <:tactic< $tac; $tacs >>) tacl 
+
+(** Dealing with conjunction *)
+
 let is_conj ist =
-  let ind = assoc_last ist in
-    if (is_conjunction ind) && (is_nodep_ind ind) (* && not (is_record ind)  *)
-      && is_binary ind (* for compatibility, as (?X _ _) matches 
-			  applications with 2 or more arguments. *)
+  let ind = assoc_var "X1" ist in
+    if (not binary_mode || is_binary ind) (* && not (is_record ind) *)
+      && is_conjunction ~strict:strict_in_hyp_and_ccl ind
     then
       <:tactic<idtac>>
     else
       <:tactic<fail>>
 
+let flatten_contravariant_conj ist =
+  let typ = assoc_var "X1" ist in
+  let c = assoc_var "X2" ist in
+  match match_with_conjunction ~strict:strict_in_contravariant_hyp typ with
+  | Some (_,args) ->
+      let i = List.length args in
+      if not binary_mode || i = 2 then 
+	let newtyp = valueIn (VConstr (List.fold_right mkArrow args c)) in
+	let intros =
+	  iter_tac (List.map (fun _ -> <:tactic< intro >>) args) 
+	  <:tactic< idtac >> in
+	<:tactic<
+          let newtyp := $newtyp in
+	  assert newtyp by ($intros; apply id; split; assumption);
+	  clear id
+	>>
+      else
+	<:tactic<fail>>
+  | _ ->
+      <:tactic<fail>>
+
+(** Dealing with disjunction *)
+
 let is_disj ist =
-  if is_disjunction (assoc_last ist) && is_binary (assoc_last ist) then
+  let t = assoc_var "X1" ist in
+  if (not binary_mode || is_binary t) &&
+    is_disjunction ~strict:strict_in_hyp_and_ccl t
+  then
     <:tactic<idtac>>
   else
     <:tactic<fail>>
 
+let flatten_contravariant_disj ist =
+  let typ = assoc_var "X1" ist in
+  let c = assoc_var "X2" ist in
+  match match_with_disjunction ~strict:strict_in_contravariant_hyp typ with
+  | Some (_,args) ->
+      let i = List.length args in
+      if not binary_mode || i = 2 then 
+	iter_tac (list_map_i (fun i arg ->
+	  let typ = valueIn (VConstr (mkArrow arg c)) in
+	  <:tactic< 
+            let typ := $typ in
+	    assert typ by (intro; apply id; constructor $i; assumption)
+	  >>) 1 args) <:tactic< clear id >>
+      else
+	<:tactic<fail>>
+  | _ ->
+      <:tactic<fail>>
+
+
+(** Main tactic *)
+
 let not_dep_intros ist =
   <:tactic<
   repeat match goal with
   | |- (?X1 -> ?X2) => intro
-  | |- (Coq.Init.Logic.iff _ _) => unfold Coq.Init.Logic.iff
-  | |- (Coq.Init.Logic.not _)   => unfold Coq.Init.Logic.not
-  | H:(Coq.Init.Logic.iff _ _)|- _ => unfold Coq.Init.Logic.iff in H
-  | H:(Coq.Init.Logic.not _)|-_    => unfold Coq.Init.Logic.not in H
-  | H:(Coq.Init.Logic.iff _ _)->_|- _ => unfold Coq.Init.Logic.iff in H
-  | H:(Coq.Init.Logic.not _)->_|-_    => unfold Coq.Init.Logic.not in H
+  | |- (Coq.Init.Logic.not _)   => unfold Coq.Init.Logic.not at 1
+  | H:(Coq.Init.Logic.not _)|-_    => unfold Coq.Init.Logic.not at 1 in H
+  | H:(Coq.Init.Logic.not _)->_|-_    => unfold Coq.Init.Logic.not at 1 in H
   end >>
 				      
 let axioms ist =
-  let t_is_unit = tacticIn is_unit
+  let t_is_unit_or_eq = tacticIn is_unit_or_eq
   and t_is_empty = tacticIn is_empty in
     <:tactic<
     match reverse goal with
-      | |- ?X1 => $t_is_unit; constructor 1
+      | |- ?X1 => $t_is_unit_or_eq; constructor 1
       | _:?X1 |- _ => $t_is_empty; elimtype X1; assumption
       | _:?X1 |- ?X1 => assumption
     end >>
 
 
 let simplif ist =
-  let t_is_unit = tacticIn is_unit
+  let t_is_unit_or_eq = tacticIn is_unit_or_eq
   and t_is_conj = tacticIn is_conj
+  and t_flatten_contravariant_conj = tacticIn flatten_contravariant_conj
+  and t_flatten_contravariant_disj = tacticIn flatten_contravariant_disj
   and t_is_disj = tacticIn is_disj
   and t_not_dep_intros = tacticIn not_dep_intros in
   <:tactic<
     $t_not_dep_intros;
     repeat
        (match reverse goal with
-        | id: (?X1 _ _) |- _ =>
-            $t_is_conj; elim id; do 2 intro; clear id
-        | id: (?X1 _ _) |- _ => $t_is_disj; elim id; intro; clear id
+        | id: ?X1 |- _ => $t_is_conj; elim id; do 2 intro; clear id
+        | id: (Coq.Init.Logic.iff _ _) |- _ => elim id; do 2 intro; clear id
+        | id: ?X1 |- _ => $t_is_disj; elim id; intro; clear id
         | id0: ?X1-> ?X2, id1: ?X1|- _ =>
 	    (* generalize (id0 id1); intro; clear id0 does not work
 	       (see Marco Maggiesi's bug PR#301)
 	    so we instead use Assert and exact. *)
 	    assert X2; [exact (id0 id1) | clear id0]
         | id: ?X1 -> ?X2|- _ =>
-          $t_is_unit; cut X2;
+          $t_is_unit_or_eq; cut X2;
 	    [ intro; clear id
 	    | (* id : ?X1 -> ?X2 |- ?X2 *)
 	      cut X1; [exact id| constructor 1; fail]
 	    ]
-        | id: (?X1 ?X2 ?X3) -> ?X4|- _ =>
-          $t_is_conj; cut (X2-> X3-> X4);
-	    [ intro; clear id
-	    | (* id: (?X1 ?X2 ?X3) -> ?X4 |- ?X2 -> ?X3 -> ?X4 *)
-	      intro; intro; cut (X1 X2 X3); [exact id| split; assumption]
-	    ]
-        | id: (?X1 ?X2 ?X3) -> ?X4|- _ =>
-          $t_is_disj;
-	    cut (X3-> X4);
-	      [cut (X2-> X4);
-	        [intro; intro; clear id
-		| (* id: (?X1 ?X2 ?X3) -> ?X4 |- ?X2 -> ?X4 *)
-		  intro; cut (X1 X2 X3); [exact id| left; assumption]
-		]
-	      | (* id: (?X1 ?X2 ?X3) -> ?X4 |- ?X3 -> ?X4 *)
-		intro; cut (X1 X2 X3); [exact id| right; assumption]
-	      ]
-        | |- (?X1 _ _) => $t_is_conj; split
+        | id: ?X1 -> ?X2|- _ =>
+          $t_flatten_contravariant_conj
+	  (* moved from "id:(?A/\?B)->?X2|-" to "?A->?B->?X2|-" *)
+        | id: (Coq.Init.Logic.iff ?X1 ?X2) -> ?X3|- _ =>
+          assert ((X1 -> X2) -> (X2 -> X1) -> X3)
+	    by (do 2 intro; apply id; split; assumption);
+            clear id
+        | id: ?X1 -> ?X2|- _ =>
+          $t_flatten_contravariant_disj
+	  (* moved from "id:(?A\/?B)->?X2|-" to "?A->?X2|-" and "?B->?X2|-" *)
+        | |- ?X1 => $t_is_conj; split
+        | |- (Coq.Init.Logic.iff _ _) => split
         end;
         $t_not_dep_intros) >>
 
@@ -153,7 +223,7 @@ let rec tauto_intuit t_reduce solver ist =
 		[ exact id
 		| generalize (fun y:X2 => id (fun x:X1 => y)); intro; clear id;
 		  solve [ $t_tauto_intuit ]]]
-      | |- (?X1 _ _) =>
+      | |- ?X1 =>
           $t_is_disj; solve [left;$t_tauto_intuit | right;$t_tauto_intuit]
       end
     ||
@@ -165,17 +235,17 @@ let rec tauto_intuit t_reduce solver ist =
     $t_solver
    ) >>
     
-let reduction_not_iff _ist =
+let reduction_not _ist =
  <:tactic<repeat 
   match goal with 
-  | |- _     => progress unfold Coq.Init.Logic.not, Coq.Init.Logic.iff 
-  | H:_ |- _ => progress unfold Coq.Init.Logic.not, Coq.Init.Logic.iff in H
+  | |- _     => progress unfold Coq.Init.Logic.not
+  | H:_ |- _ => progress unfold Coq.Init.Logic.not in H
   end >>
 
-let t_reduction_not_iff = tacticIn reduction_not_iff
+let t_reduction_not = tacticIn reduction_not
 
 let intuition_gen tac =
-  interp (tacticIn (tauto_intuit t_reduction_not_iff tac))
+  interp (tacticIn (tauto_intuit t_reduction_not tac))
 
 let simplif_gen = interp (tacticIn simplif)