- 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

1 files changed, 6 insertions, 6 deletions

diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 189c5360f1..483453cb30 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")