applyTransformation

+ we removed an Obj.magic that was casting a smaller status to a bigger status in the wrong way

components/ng_kernel/nCic.ml

@@ -121,7 +121,11 @@ type obj_kind =
  | Inductive of bool * int * inductiveType list * i_attr
                 (* true -> inductive, leftno, types *)
 
- (* the int must be 0 if the object has no body *)
+ (* the int (height) must be 0 if the object has no body *)
+ (* FG: where is this assumption used?
+    the height goes in the uri fragment of the object (def, fix)
+    but a def or a fix without a body does not exist
+ *)
 type obj = NUri.uri * int * metasenv * substitution * obj_kind
 
 (* pretty-printing *)

matita/applyTransformation.ml

@@ -23,16 +23,6 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(***************************************************************************)
-(*                                                                         *)
-(*                               PROJECT HELM                              *)
-(*                                                                         *)
-(*                   Andrea Asperti <[email protected]>                  *)
-(*                                21/11/2003                               *)
-(*                                                                         *)
-(*                                                                         *)
-(***************************************************************************)
-
 (* $Id$ *)
 
 let use_high_level_pretty_printer = ref true;; 
@@ -107,4 +97,6 @@ let notation_pp_term status term =
    BoxPp.render_to_string ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
     (function x::_ -> x | _ -> assert false) size pres
 
-let _ = NotationPp.set_pp_term (fun status y -> snd (notation_pp_term (Obj.magic status) y))
+let _ =
+  NotationPp.set_pp_term
+    (fun _status y -> snd (notation_pp_term (new status) y))