X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fmatch_concl.ml;h=078cb931a903b26ac2281d6dd8fa7b4a0236fc78;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=4f36f3ee55695705a025ee6927f2a49219834d73;hpb=5930f13b2d863abbff240ffa985bcc064c7a5ab8;p=helm.git diff --git a/helm/ocaml/tactics/match_concl.ml b/helm/ocaml/tactics/match_concl.ml index 4f36f3ee5..078cb931a 100644 --- a/helm/ocaml/tactics/match_concl.ml +++ b/helm/ocaml/tactics/match_concl.ml @@ -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