- 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

2 files changed, 47 insertions, 10 deletions

diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 189c5360f..483453cb3 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -210,12 +210,12 @@ and e_trivial_resolve db_list local_db gl =
   try 
     priority 
       (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 List.map snd (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 assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id))
@@ -412,7 +412,7 @@ and my_find_search db_list local_db hdc concl =
 
 and trivial_resolve db_list local_db cl = 
   try 
-    let hdconstr = List.hd (head_constr_bound cl []) in
+    let hdconstr = fst (head_constr_bound cl) in
     priority 
       (my_find_search db_list local_db (head_of_constr_reference hdconstr) cl)
   with Bound | Not_found -> 
@@ -424,7 +424,7 @@ and trivial_resolve db_list local_db cl =
 
 let possible_resolve db_list local_db cl =
   try 
-    let hdconstr = List.hd (head_constr_bound cl []) in
+    let hdconstr = fst (head_constr_bound cl) in
     List.map snd 
       (my_find_search db_list local_db (head_of_constr_reference hdconstr) cl)
   with Bound | Not_found -> 
@@ -432,8 +432,8 @@ let possible_resolve db_list local_db cl =
 
 let decomp_unary_term c gls = 
   let typc = pf_type_of gls c in 
-  let hd = List.hd (head_constr typc) in 
-  if Hipattern.is_conjunction hd then 
+  let t = head_constr typc in 
+  if Hipattern.is_conjunction (applist t) then 
     simplest_case c gls 
   else 
     errorlabstrm "Auto.decomp_unary_term" (str "not a unary type")
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 0bb18b3b0..535459885 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -309,6 +309,7 @@ let coq_dec_True = lazy (constant "dec_True")
 let coq_not_or = lazy (constant "not_or")
 let coq_not_and = lazy (constant "not_and")
 let coq_not_imp = lazy (constant "not_imp")
+let coq_not_iff = lazy (constant "not_iff")
 let coq_not_not = lazy (constant "not_not")
 let coq_imp_simp = lazy (constant "imp_simp")
 let coq_iff = lazy (constant "iff")
@@ -362,7 +363,7 @@ type omega_constant =
   | Eq | Neq
   | Zne | Zle | Zlt | Zge | Zgt
   | Z | Nat
-  | And | Or | False | True | Not
+  | And | Or | False | True | Not | Iff
   | Le | Lt | Ge | Gt
   | Other of string
 
@@ -388,8 +389,7 @@ let destructurate_prop t =
     | _, [_;_] when c = Lazy.force coq_Zgt -> Kapp (Zgt,args)
     | _, [_;_] when c = build_coq_and () -> Kapp (And,args)
     | _, [_;_] when c = build_coq_or () -> Kapp (Or,args)
-    | _, [t1;t2] when c = Lazy.force coq_iff -> 
-	Kapp (And,[mkArrow t1 t2;mkArrow t2 t1])
+    | _, [_;_] when c = Lazy.force coq_iff -> Kapp (Iff, args)
     | _, [_] when c = build_coq_not () -> Kapp (Not,args)
     | _, [] when c = build_coq_False () -> Kapp (False,args)
     | _, [] when c = build_coq_True () -> Kapp (True,args)
@@ -1557,6 +1557,9 @@ let rec decidability gl t =
     | Kapp(And,[t1;t2]) -> 
 	mkApp (Lazy.force coq_dec_and, [| t1; t2;
 		  decidability gl t1; decidability gl t2 |])
+    | Kapp(Iff,[t1;t2]) -> 
+	mkApp (Lazy.force coq_dec_iff, [| t1; t2;
+		  decidability gl t1; decidability gl t2 |])
     | Kimp(t1,t2) -> 
 	mkApp (Lazy.force coq_dec_imp, [| t1; t2;
 		  decidability gl t1; decidability gl t2 |])
@@ -1620,6 +1623,30 @@ let destructure_hyps gl =
 		    (introduction i2);
 		    (loop ((i1,None,t1)::(i2,None,t2)::lit)) ] gl)
 	      ]
+          | Kapp(Iff,[t1;t2]) ->
+              tclTHENLIST [
+                (elim_id i);
+		(tclTRY (clear [i]));
+		(fun gl -> 
+		  let i1 = fresh_id [] (add_suffix i "_left") gl in
+		  let i2 = fresh_id [] (add_suffix i "_right") gl in
+		  tclTHENLIST [
+		    introduction i1;
+		    generalize_tac
+		      [mkApp (Lazy.force coq_imp_simp,
+                        [| t1; t2; decidability gl t1; mkVar i1|])];
+		    onClearedName i1 (fun i1 ->
+		      tclTHENLIST [
+			introduction i2;
+			generalize_tac
+			  [mkApp (Lazy.force coq_imp_simp,
+                            [| t2; t1; decidability gl t2; mkVar i2|])];
+			onClearedName i2 (fun i2 ->
+			  loop
+			  ((i1,None,mk_or (mk_not t1) t2)::
+			   (i2,None,mk_or (mk_not t2) t1)::lit))
+		      ])] gl)
+	      ]
           | Kimp(t1,t2) ->
               if
                 is_Prop (pf_type_of gl t1) &
@@ -1647,10 +1674,20 @@ let destructure_hyps gl =
                     tclTHENLIST [
 		      (generalize_tac
 		        [mkApp (Lazy.force coq_not_and, [| t1; t2;
-			  decidability gl t1;mkVar i|])]);
+			  decidability gl t1; mkVar i|])]);
 		      (onClearedName i (fun i ->
                         (loop ((i,None,mk_or (mk_not t1) (mk_not t2))::lit))))
                     ]
+		| Kapp(Iff,[t1;t2]) ->
+                    tclTHENLIST [
+		      (generalize_tac
+		        [mkApp (Lazy.force coq_not_iff, [| t1; t2;
+			  decidability gl t1; decidability gl t2; mkVar i|])]);
+		      (onClearedName i (fun i ->
+                        (loop ((i,None,
+			        mk_or (mk_and t1 (mk_not t2))
+				      (mk_and (mk_not t1) t2))::lit))))
+                    ]
 		| Kimp(t1,t2) ->
                     tclTHENLIST [
 		      (generalize_tac