module Ast = NotationPt
module NRef = NReference
-let debug_print s = prerr_endline (Lazy.force s);;
-let debug_print _ = ();;
+let debug = ref false;;
+let debug_print s = if !debug then prerr_endline (Lazy.force s);;
let cic_name_of_name = function
| Ast.Ident (n, None) -> n
let refine_obj status metasenv subst _context _uri ~use_coercions obj _ _ugraph
~localization_tbl
=
+ (*prerr_endline ((sprintf "TEST_INTERPRETATION: %s" (status#ppobj obj)));*)
assert (metasenv=[]);
assert (subst=[]);
let localise t =