new tactics are almost ready

[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 83422cd8f238ee1f207afb8931f57bcb2d7b16c4..c4c66374a622b59965efdf611d262aa495732bde 100644 (file)
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -172,37 +172,6 @@ let ppterm ~context ~subst ~metasenv ?(margin=80) ?inside_fix t =
   ppterm ~context ~subst ~metasenv ?inside_fix t
 ;;
 
-
-let ppobj = function
-  | (u,_,metasenv,subst,NCic.Fixpoint (b, fl, _)) -> 
-      "{"^NUri.string_of_uri u^"}\n"^
-      (if b then "let rec " else "let corec ") ^
-       String.concat "\nand " 
-        (List.map (fun (_,name,n,ty,bo) ->
-          name^ " on " ^ string_of_int n ^ " : " ^ 
-          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^"} with "^string_of_int leftno^" fixed params\n"^
-      (if b then "inductive " else "coinductive ")^
-      String.concat "\nand "
-        (List.map (fun (_,name,ty,cl) ->
-          name^": "^ppterm ~metasenv ~subst ~context:[] ty^ " :=\n"^
-          String.concat "\n"
-          (List.map (fun (_,name,ty) ->
-           "  | "^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"
-;;
-
 let rec ppcontext ?(sep="\n") ~subst ~metasenv = function
   | [] -> ""
   | (name, NCic.Decl t) :: tl -> 
@@ -240,5 +209,38 @@ let rec ppsubst ~subst ~metasenv = function
 
 let ppsubst ~metasenv subst = ppsubst ~metasenv ~subst subst;;
 
+
+let ppobj (u,_,metasenv, subst, o) = 
+  "metasenv:\n" ^ ppmetasenv ~subst metasenv ^ "\n" ^
+  match o with 
+  | NCic.Fixpoint (b, fl, _) -> 
+      "{"^NUri.string_of_uri u^"}\n"^
+      (if b then "let rec " else "let corec ") ^
+       String.concat "\nand " 
+        (List.map (fun (_,name,n,ty,bo) ->
+          name^ " on " ^ string_of_int n ^ " : " ^ 
+          ppterm ~metasenv ~subst ~context:[] ty ^ " :=\n"^
+          ppterm ~metasenv ~subst ~context:[] ~inside_fix:true bo) fl)
+  | NCic.Inductive (b, leftno,tyl, _) -> 
+      "{"^NUri.string_of_uri u^"} with "^string_of_int leftno^" fixed params\n"^
+      (if b then "inductive " else "coinductive ")^
+      String.concat "\nand "
+        (List.map (fun (_,name,ty,cl) ->
+          name^": "^ppterm ~metasenv ~subst ~context:[] ty^ " :=\n"^
+          String.concat "\n"
+          (List.map (fun (_,name,ty) ->
+           "  | "^name^": "^ppterm ~metasenv ~subst ~context:[] ty)
+           cl)) tyl) ^ "."
+  | NCic.Constant (_,name,None,ty, _) -> 
+      "{"^NUri.string_of_uri u^"}\n"^
+        "axiom " ^ name ^ " : " ^ 
+          ppterm ~metasenv ~subst ~context:[] ty ^ "\n" 
+  | 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"
+;;
+
 let _ = NCicSubstitution.set_ppterm (ppterm ~margin:80);;