snapshot

[helm.git] / helm / ocaml / cic_notation / cicNotationRew.ml

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index 180a8c912f05484c451d856c30a3151586b71b58..f3f6cac2a75267da7d44ecddc3c10810a5de3820 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -118,7 +118,6 @@ let pp_ast0 t k =
   aux t
 
 let ast_of_acic0 term_info acic k =
-(*   prerr_endline "ast_of_acic0"; *)
   let k = k term_info in
   let register_uri id uri = Hashtbl.add term_info.uri id uri in
   let sort_of_id id =
@@ -265,7 +264,6 @@ let instantiate21 env (* precedence associativity *) l1 =
     | Ast.AttributedTerm (_, t) -> subst env t
     | Ast.Variable var ->
         let name, expected_ty = CicNotationEnv.declaration_of_var var in
-         prerr_endline ("searching for " ^ name);
         let ty, value =
           try
             List.assoc name env
@@ -357,15 +355,9 @@ let rec pp_ast1 term =
                  Hashtbl.find level1_patterns21 pid
                with Not_found -> assert false
               in
-               prerr_endline ("IN " ^ CicNotationPp.pp_term term);
-               (* LUCA: il termine legato e' lo stesso termine di partenza per cui si innesca il loop infinito *)
-               let res = Ast.AttributedTerm (`Level (precedence, associativity),
-                                             (instantiate21 (ast_env_of_env env) l1))
-               in
-                 prerr_endline "OUT";
-                 res
+               Ast.AttributedTerm (`Level (precedence, associativity),
+                               (instantiate21 (ast_env_of_env env) l1))
       end
-  
 
 let instantiate32 term_info env symbol args =
   let rec instantiate_arg = function