From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 5 Nov 2007 14:29:47 +0000 (+0000)
Subject: Obj.magic are now generated to extract dependently typed MutCases.
X-Git-Tag: make_still_working~5898
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1d3a609d2c031828553e33f59b4db42a5b9ff46f;p=helm.git

Obj.magic are now generated to extract dependently typed MutCases.
---

diff --git a/helm/software/components/METAS/meta.helm-cic_exportation.src b/helm/software/components/METAS/meta.helm-cic_exportation.src
index 97124f913..f73bbeb64 100644
--- a/helm/software/components/METAS/meta.helm-cic_exportation.src
+++ b/helm/software/components/METAS/meta.helm-cic_exportation.src
@@ -1,4 +1,4 @@
-requires="helm-cic_proof_checking"
+requires="helm-cic_acic"
 version="0.0.1"
 archive(byte)="cic_exportation.cma"
 archive(native)="cic_exportation.cmxa"
diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml
index 7be9ea3d9..79eab870d 100644
--- a/helm/software/components/cic_exportation/cicExportation.ml
+++ b/helm/software/components/cic_exportation/cicExportation.ml
@@ -229,6 +229,11 @@ let rec pp t context =
            string_of_int n2
        )
     | C.MutCase (uri,n1,ty,te,patterns) ->
+       let needs_obj_magic =
+        match ty with
+           Cic.Lambda (_,_,t) -> not (DoubleTypeInference.does_not_occur 1 t)
+         | _ -> assert false
+       in
        let paramsno =
         match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
            C.InductiveDefinition (_,_,paramsno,_) -> paramsno
@@ -307,7 +312,11 @@ let rec pp t context =
                          x ^ (if sargs = "" then "" else "(" ^ sargs^ ")"),
                           body
                       in
-                       pattern ^ " -> " ^ body
+                       pattern ^ " -> " ^
+                        if needs_obj_magic then
+                         "Obj.magic (" ^ body ^ ")"
+                        else
+                         body
                    ) connames_and_argsno_and_patterns)) ^
                  ")\n"))
     | C.Fix (no, funs) ->