Arguments of constructors in a case pattern are now ppid-ed.

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

diff --git a/components/cic_exportation/cicExportation.ml b/components/cic_exportation/cicExportation.ml
index 9296b7bb05d260fd4429147b12c354104070a95c..e671effca9a565645d8d7f8c41f780d8b13f5d38 100644 (file)
--- a/components/cic_exportation/cicExportation.ml
+++ b/components/cic_exportation/cicExportation.ml
@@ -238,9 +238,10 @@ let rec pp ~in_type t context =
         "unit (* TOO POLYMORPHIC TYPE *)"
        else (
        let needs_obj_magic =
-        match ty with
+        (* BUG HERE: we should consider also the right parameters *)
+        match CicReduction.whd context ty with
            Cic.Lambda (_,_,t) -> not (DoubleTypeInference.does_not_occur 1 t)
-         | _ -> assert false
+         | _ -> false (* it can be a Rel, e.g. in *_rec *)
        in
        (match analyze_term context te with
            `Type -> assert false
@@ -293,6 +294,10 @@ let rec pp ~in_type t context =
                      let rec aux argsno context =
                       function
                          Cic.Lambda (name,ty,bo) when argsno > 0 ->
+                          let name =
+                           match name with
+                              Cic.Anonymous -> Cic.Anonymous
+                            | Cic.Name n -> Cic.Name (ppid n) in
                           let args,res =
                            aux (argsno - 1) (Some (name,Cic.Decl ty)::context)
                             bo