]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/match_concl.ml
- some code patched
[helm.git] / helm / ocaml / tactics / match_concl.ml
index 4f36f3ee55695705a025ee6927f2a49219834d73..078cb931a903b26ac2281d6dd8fa7b4a0236fc78 100644 (file)
@@ -171,8 +171,10 @@ let cmatch (conn:Mysql.dbd) t =
     let prefixes = NewConstraints.prefixes just_factor t in
     (match prefixes with
         Some main, all_concl ->
+(*      
            NewConstraints.pp_prefixes all_concl;
-          (* in some cases, max_prefix_length could be less than n *)
+*)
+           (* in some cases, max_prefix_length could be less than n *)
           let max_prefix_length = 
             match all_concl with
                 [] -> assert false