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

[helm.git] / components / cic_exportation / cicExportation.ml

diff --git a/components/cic_exportation/cicExportation.ml b/components/cic_exportation/cicExportation.ml
index 7be9ea3d9f0e30b566fb67e1e6b793b86b76d9f5..79eab870d2c9a7c421c3f1cdfed5d2b7f61c1946 100644 (file)
--- a/components/cic_exportation/cicExportation.ml
+++ b/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) ->