From: Claudio Sacerdoti Coen Date: Mon, 5 Nov 2007 14:29:47 +0000 (+0000) Subject: Obj.magic are now generated to extract dependently typed MutCases. X-Git-Tag: 0.4.95@7852~49 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d49dfa3ac124025413d17c02da9b0486d8c765d5;p=helm.git Obj.magic are now generated to extract dependently typed MutCases. --- diff --git a/components/METAS/meta.helm-cic_exportation.src b/components/METAS/meta.helm-cic_exportation.src index 97124f913..f73bbeb64 100644 --- a/components/METAS/meta.helm-cic_exportation.src +++ b/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/components/cic_exportation/cicExportation.ml b/components/cic_exportation/cicExportation.ml index 7be9ea3d9..79eab870d 100644 --- 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) ->