Capitalization of variables bound in patterns 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 6b797ef449beb26978929f8a5ed113b57e695c99..5690d1c9f7f58da6fc55fa69c65dfe73a4ceeb77 100644 (file)
--- a/matita/components/ng_kernel/nCicExtraction.ml
+++ b/matita/components/ng_kernel/nCicExtraction.ml
@@ -716,7 +716,6 @@ let object_of_inductive status ~metasenv uri ind leftno il =
           let right,left = HExtlib.split_nth (List.length ctx - leftno) ctx in
           let ref =
            NReference.reference_of_spec uri (NReference.Ind (ind,i,leftno)) in
-prerr_endline ("AGGIUNGO" ^ NReference.string_of_reference ref);
           let info = ref,(ctx,None) in
           let status =
            status#set_extraction_db
@@ -929,8 +928,11 @@ let pretty_print_term_context status ctx1 ctx2 =
     (fun el (ctx1,rev_res) ->
       match el with
          None -> ""@::ctx1,rev_res
-       | Some (name,`OfKind _) -> name@::ctx1,rev_res
+       | Some (name,`OfKind _) ->
+          let name = capitalize `TypeVariable name in
+           name@::ctx1,rev_res
        | Some (name,`OfType typ) ->
+          let name = capitalize `TypeVariable name in
           let name,ctx1 = name@:::ctx1 in
            name::ctx1,
             ("(" ^ name ^ " :: " ^ pretty_print_type status ctx1 typ ^ ")")::rev_res
@@ -960,8 +962,8 @@ let rec pretty_print_term status ctxt =
       if pl = [] then
        "error \"Case analysis over empty type\""
       else
-       "case " ^ pretty_print_term status ctxt matched ^ " of\n" ^
-         String.concat "\n"
+       "case " ^ pretty_print_term status ctxt matched ^ " of {\n" ^
+         String.concat " ;\n"
            (HExtlib.list_mapi
              (fun (bound_names,rhs) i ->
                let ref = NReference.mk_constructor (i+1) r in
@@ -972,7 +974,7 @@ let rec pretty_print_term status ctxt =
                 pretty_print_term status ctxt rhs
                in
                  "  " ^ name ^ " " ^ bound_names ^ " -> " ^ body
-             ) pl)
+             ) pl) ^ "}\n  "
     | Skip t -> pretty_print_term status ("[[skipped]]"@::ctxt) t
     | TLambda (name,t) ->
        let name = capitalize `TypeVariable name in
@@ -1032,8 +1034,8 @@ let rec pp_obj status (_,ref,obj_kind) =
            let namectx = namectx_of_ctx left in
             pp_ref status ref ^ " :: " ^
              pretty_print_type status namectx tys
-         ) cl
-      )) il)
+         ) cl) ^ "\n    deriving (Prelude.Show)"
+      ) il)
  (* inductive and records missing *)
 
 let rec infos_of (info,_,obj_kind) =