Petites corrections vis à vis des commits 10860, 10859, 10850

- pour le "try", la nouvelle erreur CannotFindWellTypedAbstraction
  doit être catchable
- pour accomoder Type -1 dans le discharge, il faut un refresh_universes strict
- bugs dans les fichiers de test-suite


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

2 files changed, 7 insertions, 2 deletions

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index a81f68b79..124637e13 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -160,15 +160,19 @@ let new_Type_sort () = Type (new_univ ())
 (* This refreshes universes in types; works only for inferred types (i.e. for
    types of the form (x1:A1)...(xn:An)B with B a sort or an atom in
    head normal form) *)
-let refresh_universes t =
+let refresh_universes_gen strict t =
   let modified = ref false in
   let rec refresh t = match kind_of_term t with
-    | Sort (Type u) when u <> Univ.lower_univ -> modified := true; new_Type ()
+    | Sort (Type u) when strict or u <> Univ.lower_univ ->
+	modified := true; new_Type ()
     | Prod (na,u,v) -> mkProd (na,u,refresh v)
     | _ -> t in
   let t' = refresh t in
   if !modified then t' else t
 
+let refresh_universes = refresh_universes_gen false
+let refresh_universes_strict = refresh_universes_gen true
+
 let new_sort_in_family = function 
   | InProp -> prop_sort
   | InSet -> set_sort
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 64edcd2e3..ded85464e 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -21,6 +21,7 @@ val new_sort_in_family : sorts_family -> sorts
 val new_Type : unit -> types
 val new_Type_sort : unit -> sorts
 val refresh_universes : types -> types
+val refresh_universes_strict : types -> types
 
 (* printers *)
 val print_sort : sorts -> std_ppcmds