]> matita.cs.unibo.it Git - helm.git/commitdiff
Debugging code removed.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 26 Nov 2005 16:41:01 +0000 (16:41 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 26 Nov 2005 16:41:01 +0000 (16:41 +0000)
helm/ocaml/cic_unification/cicRefine.ml

index 2b4b68947b9ca8025edf0dd174761b5cb6ca4db1..f050726bcc70034f6844e1ebc110ab3fc71c424c 100644 (file)
@@ -852,7 +852,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
         | (uri,t)::tl ->
             let ty_uri,ugraph1 =  type_of_variable uri ugraph in
             let typeofvar =
-prerr_endline ("<<<" ^ CicPp.ppterm ty_uri);
               CicSubstitution.subst_vars substs ty_uri in
               (* CSC: why was this code here? it is wrong
                  (match CicEnvironment.get_cooked_obj ~trust:false uri with