From 10c62d5b6703eddbc83b011b73f9540e47a2001f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 30 May 2011 11:02:26 +0000 Subject: [PATCH] Debugging code to understand cases where the output notation is not applied, is applied badly or it raises an assert failure. Usually the problem is given by optional parts of the term. For instance, in output all typing information is present and it _must_ be matched. --- matita/components/content_pres/content2presMatcher.ml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/matita/components/content_pres/content2presMatcher.ml b/matita/components/content_pres/content2presMatcher.ml index 8b613a524..ee62e06e6 100644 --- a/matita/components/content_pres/content2presMatcher.ml +++ b/matita/components/content_pres/content2presMatcher.ml @@ -105,7 +105,7 @@ struct name, (Env.NumType, Env.NumValue s) | Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, None)) -> name, (Env.StringType, Env.StringValue (Env.Ident s)) - | _ -> assert false) + | _ -> assert false (* activate the DEBUGGING CODE below *)) pl tl with Invalid_argument _ -> assert false @@ -157,7 +157,16 @@ struct in magichooser candidates in +(* DEBUGGING CODE +fun input -> +let (fst,_)::_ = rows in +prerr_endline ("RIGA: " ^ NotationPp.pp_term (new NCicPp.status) fst); +prerr_endline ("CONTRO: " ^ NotationPp.pp_term (new NCicPp.status) input); +*) M.compiler rows' match_cb (fun _ -> None) +(* DEBUGGING CODE +input +*) and compile_magic = function | Ast.Fold (kind, p_base, names, p_rec) -> -- 2.39.2