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 97124f91373eb10434aa5fa40edaf363240d9a73..f73bbeb64facf4c6170598b05e5b4fa3329bcc16 100644 (file)
--- 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 7be9ea3d9f0e30b566fb67e1e6b793b86b76d9f5..79eab870d2c9a7c421c3f1cdfed5d2b7f61c1946 100644 (file)
--- 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) ->