Appl case in is_really_smaller fixed as in the old kernel

[helm.git] / helm / software / components / ng_kernel / nCicPp.ml

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 8bcbf6ad9755d0a5fc43a7a5cc686f09e0c8ffbe..72e8abff5347e9d41c34bf933aa3016c0d3a3959 100644 (file)
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -139,8 +139,8 @@ let ppobj = function
           ppterm ~metasenv ~subst ~context:[] ty ^ " :=\n"^
           ppterm ~metasenv ~subst ~context:[] ~inside_fix:true bo) fl)
   | (u,_,metasenv,subst,NCic.Inductive (b, leftno,tyl, _)) -> 
-      "{"^NUri.string_of_uri u^"}\n"^
-      "inductive ("^string_of_int leftno^") "^
+      "{"^NUri.string_of_uri u^"} with "^string_of_int leftno^" fixed params\n"^
+      "inductive "^
       String.concat "\nand "
         (List.map (fun (_,name,ty,cl) ->
           name^": "^ppterm ~metasenv ~subst ~context:[] ty^ " :=\n"^
@@ -149,9 +149,11 @@ let ppobj = function
            "  | "^name^": "^ppterm ~metasenv ~subst ~context:[] ty)
            cl)) tyl) ^ "."
   | (u,_,metasenv,subst,NCic.Constant (_,name,None,ty, _)) -> 
+      "{"^NUri.string_of_uri u^"}\n"^
         "axiom " ^ name ^ " : " ^ 
           ppterm ~metasenv ~subst ~context:[] ty ^ "\n"
   | (u,_,metasenv,subst,NCic.Constant (_,name,Some bo,ty, _)) ->
+      "{"^NUri.string_of_uri u^"}\n"^
         "definition " ^ name ^ " : " ^ 
           ppterm ~metasenv ~subst ~context:[] ty ^ " := \n"^
           ppterm ~metasenv ~subst ~context:[] bo ^ "\n"