Pretty printing of context (variable refreshing) fixed.

[helm.git] / matita / components / ng_kernel / nCicExtraction.ml

diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml
index 691d8143dfcf63617b85414040810d3ebb79d98a..6a642390efb1a949d91170bc8e368ce1ae52befd 100644 (file)
--- a/matita/components/ng_kernel/nCicExtraction.ml
+++ b/matita/components/ng_kernel/nCicExtraction.ml
@@ -73,10 +73,10 @@ let rec size_of_type =
     | Unit -> 1
     | Top -> 1
     | TConst c -> 1
-    | Arrow (l, r) -> 1 + size_of_type l + size_of_type r
+    | Arrow _ -> 2
     | Skip t -> size_of_type t
-    | Forall (name, kind, typ) -> 1 + size_of_type typ
-    | TAppl l -> List.fold_right (+) (List.map size_of_type l) 0
+    | Forall _ -> 2
+    | TAppl l -> 1
 ;;
 
 type term =
@@ -748,6 +748,9 @@ let rec pretty_print_term status ctxt =
     | LetIn (name,s,t) ->
       "let " ^ name ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^ pretty_print_term status (name@::ctxt) t
     | Match (r,matched,pl) ->
+      if pl = [] then
+       "error \"Case analysis over empty type\""
+      else
       let constructors, leftno =
       let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status r in
       let _,_,_,cl  = List.nth tys n in
@@ -793,15 +796,15 @@ type term_former_decl = term_context * typ
 
 let rec pp_obj status (uri,obj_kind) =
   let pretty_print_context ctx =
-    String.concat " " (List.rev
+    String.concat " " (List.rev (snd
       (List.fold_right
-       (fun (x,kind) l ->
+       (fun (x,kind) (l,res) ->
          let x,l = x @:::l in
          if size_of_kind kind > 1 then
-          ("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::l
+          x::l,("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::res
          else
-          x::l)
-       (HExtlib.filter_map (fun x -> x) ctx) []))
+          x::l,x::res)
+       (HExtlib.filter_map (fun x -> x) ctx) ([],[]))))
   in
  let namectx_of_ctx ctx =
   List.fold_right (@::)