The innersort is now computed as the more precise sort between the

synthesized innersort and the expected innersort.
This closes a bug that allowed to export non well-typed* terms like the
following one:

  ((fun (X : (T1 : CProp)) => (E : (T2 : Type))) : (T1 -> T2 : CProp))

* non well-typed according to the rules that consider CProp as a primitive
  sort.


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

1 files changed, 15 insertions, 1 deletions

diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index ec5ccc8e5..b15611438 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -396,7 +396,21 @@ print_endline "ENVIRONMENT:" ; flush stdout ;
 Pp.ppnl (Printer.pr_context_of env) ; flush stdout ;
 print_endline "FINE_ENVIRONMENT" ; flush stdout ;
 *)
-         let innersort = get_sort_family_of env evar_map synthesized in
+         let innersort =
+          let synthesized_innersort =
+           get_sort_family_of env evar_map synthesized
+          in
+           match expected with
+              None -> synthesized_innersort
+            | Some ty ->
+              let expected_innersort =
+               get_sort_family_of env evar_map ty
+              in
+               match expected_innersort, synthesized_innersort with
+                  CProp, _
+                | _, CProp -> CProp
+                | _, _ -> expected_innersort
+         in
 (* Debugging only:
 print_endline "PASSATO" ; flush stdout ;
 *)