X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_exportation%2FcicExportation.ml;h=f35cd0e1e73d71996cb46770f5cae758795cc49e;hb=475dce2026d582f3a7829599dc8cfddb865d4640;hp=813e65c298bf9c5c9281597088dadf655b7db3e6;hpb=8896b5179a1b8b0fa6f9b26bb3142fdaf863276f;p=helm.git

diff --git a/components/cic_exportation/cicExportation.ml b/components/cic_exportation/cicExportation.ml
index 813e65c29..f35cd0e1e 100644
--- a/components/cic_exportation/cicExportation.ml
+++ b/components/cic_exportation/cicExportation.ml
@@ -45,8 +45,7 @@ let analyze_type context t =
  let rec aux =
   function
      Cic.Sort s -> `Sort s
-   | Cic.Prod (_,_,t)
-   | Cic.Lambda (_,_,t) -> aux t
+   | Cic.Prod (_,_,t) -> aux t
    | _ -> `SomethingElse
  in
  match aux t with
@@ -63,7 +62,9 @@ let ppid =
  let reserved =
   [ "to";
     "mod";
-    "val"
+    "val";
+    "in";
+    "function"
   ]
  in
   function n ->