From 7b7bbf9aeb778e8e27f76e1770a45979a213eb86 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Wed, 8 Sep 2004 14:29:45 +0000
Subject: 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
---
 contrib/xml/cic2acic.ml | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index ec5ccc8e53..b156114380 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 ;
 *)
-- 
cgit v1.2.3