From c137ba88f68a47e567077909a23993c3c8c9854d Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 19 Feb 2004 08:27:20 +0000 Subject: [PATCH] Minor modification in test_parser (to use the new pretty printer for tacticals). --- helm/ocaml/cic_disambiguation/test_parser.ml | 7 ++++++- helm/ocaml/cic_disambiguation/tests/match.txt | 6 ++++++ 2 files changed, 12 insertions(+), 1 deletion(-) diff --git a/helm/ocaml/cic_disambiguation/test_parser.ml b/helm/ocaml/cic_disambiguation/test_parser.ml index 4937f4ca4..d6afddc67 100644 --- a/helm/ocaml/cic_disambiguation/test_parser.ml +++ b/helm/ocaml/cic_disambiguation/test_parser.ml @@ -27,6 +27,11 @@ let default_mode = `Term let mode = ref default_mode +(* let pp_tactical = TacticAstPp.pp_tactical *) + +let pp_tactical = TacticAst2Box.tacticalPp + + let _ = try match Sys.argv.(1) with @@ -55,7 +60,7 @@ let _ = print_endline (TacticAstPp.pp_tactic term) | `Tactical -> let term = CicTextualParser2.parse_tactical istream in - print_endline (TacticAstPp.pp_tactical term) + print_endline (pp_tactical term) | `Alias -> let env = CicTextualParser2.EnvironmentP3.of_string line in print_endline (CicTextualParser2.EnvironmentP3.to_string env)); diff --git a/helm/ocaml/cic_disambiguation/tests/match.txt b/helm/ocaml/cic_disambiguation/tests/match.txt index 8acbb1350..87bb0159b 100644 --- a/helm/ocaml/cic_disambiguation/tests/match.txt +++ b/helm/ocaml/cic_disambiguation/tests/match.txt @@ -10,6 +10,11 @@ match (le_n O): le with [ le_n \Rightarrow (refl_equal nat O) | (le_S x y) \Rightarrow (refl_equal nat O) ] +[\lambda z:nat. \lambda h:(le (plus (plus O O) (plus O O)) z). (eq nat (plus (plus O O) (plus O O)) (plus (plus O O) (plus O O)))] +match (le_n (plus (plus O O) (plus O O))): le with +[ le_n \Rightarrow (refl_equal nat (plus (plus O O) (plus O O))) +| (le_S x y) \Rightarrow (refl_equal nat (plus (plus O O) (plus O O))) ] + (* [\lambda z:nat. \lambda h:(le 1 z). (le 0 z)] match (le_S 2 (le_n 1)): le with @@ -22,6 +27,7 @@ match (le_S 0 0 (le_n 0)): le with [ le_n \Rightarrow (le_S 0 0 (le_n 0)) | (le_S x y) \Rightarrow (le_S 0 (S x) (le_S 0 x y)) ] + [\lambda x:bool. nat] match true:bool with [ true \Rightarrow O -- 2.39.2