From f5eb06f0d2b28fe72db12fb57458b961b9ae9d85 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 28 Dec 2008 19:03:04 +0000
Subject: - 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
---
 contrib/interface/blast.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'contrib/interface')

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")
-- 
cgit v1.2.3