From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 4 Nov 2007 17:44:37 +0000 (+0000)
Subject: * type definitions that define a new proposition are no longer exported
X-Git-Tag: 0.4.95@7852~62
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a6a216d3c7e56c5b282841bb42b1fc0dd4c0150a;p=helm.git

* type definitions that define a new proposition are no longer exported
* type arguments of type Prop are no longer abstracted in inductive types
---

diff --git a/components/cic_exportation/cicExportation.ml b/components/cic_exportation/cicExportation.ml
index b493c4e40..06fc38308 100644
--- a/components/cic_exportation/cicExportation.ml
+++ b/components/cic_exportation/cicExportation.ml
@@ -44,12 +44,12 @@ let analyze_term context t =
 let analyze_type context t =
  let rec aux =
   function
-     Cic.Sort _ -> `Sort
+     Cic.Sort s -> `Sort s
    | Cic.Prod (_,_,t) -> aux t
    | _ -> `SomethingElse
  in
  match aux t with
-    `Sort -> `Sort
+    `Sort _ as res -> res
   | `SomethingElse ->
       match
        fst(CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph)
@@ -168,7 +168,7 @@ let rec pp t context =
     | C.Cast (v,t) -> pp v context
     | C.Lambda (b,s,t) ->
        (match analyze_type context s with
-           `Sort
+           `Sort _
          | `Statement -> pp t ((Some (b,Cic.Decl s))::context)
          | `Type -> "(function " ^ ppname b ^ " -> " ^ pp t ((Some (b,Cic.Decl s))::context) ^ ")")
     | C.LetIn (b,s,t) ->
@@ -333,8 +333,9 @@ let ppinductiveType current_module_name (typename, inductive, arity, cons) =
       function
          Cic.Prod (n,s,t) ->
            (match analyze_type context s with
-               `Statement
-             | `Sort ->
+               `Sort Cic.Prop -> args ((Some (n,Cic.Decl s))::context) t
+             | `Statement
+             | `Sort _ ->
                  let n =
                   match n with
                      Cic.Anonymous -> Cic.Anonymous
@@ -371,13 +372,15 @@ let ppobj current_module_name obj =
   match obj with
     C.Constant (name, Some t1, t2, params, _) ->
       (match analyze_type [] t2 with
-          `Statement -> ""
+          `Sort Cic.Prop
+        | `Statement -> ""
         | `Type
-        | `Sort -> "let " ^ ppid name ^ " =\n" ^ pp t1 [] ^ "\n")
+        | `Sort _ -> "let " ^ ppid name ^ " =\n" ^ pp t1 [] ^ "\n")
    | C.Constant (name, None, ty, params, _) ->
       (match analyze_type [] ty with
-          `Statement -> ""
-        | `Sort -> "type " ^ ppid name ^ "\n"
+          `Sort Cic.Prop
+        | `Statement -> ""
+        | `Sort _ -> "type " ^ ppid name ^ "\n"
         | `Type -> "let " ^ ppid name ^ " = assert false\n")
    | C.Variable (name, bo, ty, params, _) ->
       "Variable " ^ name ^