- 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, 6 insertions, 2 deletions

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 996c00eba..689257c3b 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -591,7 +591,8 @@ let lookup_eliminator ind_sp s =
     errorlabstrm "default_elim"
       (strbrk "Cannot find the elimination combinator " ++
        pr_id id ++ strbrk ", the elimination of the inductive definition " ++
-       pr_id id ++ strbrk " on sort " ++ pr_sort_family s ++
+       pr_global_env Idset.empty (IndRef ind_sp) ++ 
+       strbrk " on sort " ++ pr_sort_family s ++
        strbrk " is probably not allowed.")
 
 
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 123ff43e7..532c258fa 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -115,8 +115,11 @@ let retype sigma metamap =
 	let s2 = sort_family_of (push_rel (name,None,t) env) c2 in
 	if Environ.engagement env <> Some ImpredicativeSet &&
 	   s2 = InSet & sort_family_of env t = InType then InType else s2
+    | App(f,args) when isGlobalRef f ->
+	let t = type_of_global_reference_knowing_parameters env f args in
+        family_of_sort (sort_of_atomic_type env sigma t args)
     | App(f,args) -> 
-       family_of_sort (sort_of_atomic_type env sigma (type_of env f) args)
+	family_of_sort (sort_of_atomic_type env sigma (type_of env f) args)
     | Lambda _ | Fix _ | Construct _ ->
         anomaly "sort_of: Not a type (1)"
     | _ -> family_of_sort (decomp_sort env sigma (type_of env t))