From ff2600a4e94b4ca565285b8d3ca7f5cb2ec725da Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 7 Oct 2022 21:41:18 -0400
Subject: [PATCH] test: add test for proof syntax

---
 unittest/parser/p1.ml | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/unittest/parser/p1.ml b/unittest/parser/p1.ml
index 0b762214..abc7631d 100644
--- a/unittest/parser/p1.ml
+++ b/unittest/parser/p1.ml
@@ -43,7 +43,9 @@ let test_decl what s =
   | Ok l ->
     Fmt.printf "@[<v2>%s:@ %a@]@." what (Util.pp_list ~sep:"" A.pp_decl) l
   | Error err ->
-    Fmt.printf "FAIL:@ error while parsing %S:@ %a@." what P.Error.pp err
+    Fmt.printf "FAIL:@ error while parsing %S:@ %a@." what
+      (P.Error.pp_with_loc ~input:(Loc.Input.string s))
+      err
 
 let () =
   test_decl "d1"
@@ -51,3 +53,11 @@ let () =
     #ty f;
     #sledgehammer fn x y. f x y = f x y;
   |}
+
+let () =
+  test_decl "d2"
+    {|theorem foo := (a=b) => (f a = f b)
+       { have s1 := b=a by obvious;
+         have s2 := f b = f a by congr f s1;
+         exact symm s2
+       }; |}