Fix issue #1001 (#1087)

With the invaluable help of Michael Faerber Co-authored-by: Gabriel Hondet <[email protected]> Co-authored-by: Frédéric Blanqui <[email protected]>
Deducteam · Apr 23, 2024 · 51263d6 · 51263d6
1 parent 49fb1e3
commit 51263d6
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/src/parsing/lpParser.mly b/src/parsing/lpParser.mly
@@ -220,7 +220,7 @@ path:
   | p=QID { make_pos $sloc (List.rev p) }
 
 modifier:
-  | d=SIDE? ASSOCIATIVE
+  | d=ioption(SIDE) ASSOCIATIVE
     { let b = match d with Some Pratter.Left -> true | _ -> false in
       make_pos $sloc (P_prop (Term.Assoc b)) }
   | COMMUTATIVE { make_pos $sloc (P_prop Term.Commu) }

diff --git a/tests/OK/iss1001.lp b/tests/OK/iss1001.lp
@@ -0,0 +1,3 @@
+constant symbol A : TYPE;
+
+associative commutative symbol * : A → A → A;
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		constant symbol A : TYPE;

		associative commutative symbol * : A → A → A;