Commit c9e5da79 authored by MARCHE Claude's avatar MARCHE Claude

transformations: fix parsing of args of type termlist

parent 353247c8
......@@ -352,13 +352,9 @@
<goal name="VC lrs.20" expl="postcondition" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="VC lrs.20.0" expl="postcondition" proved="true">
<transf name="instantiate" proved="true" arg1="H7" arg2="x">
<transf name="instantiate" proved="true" arg1="H7" arg2="x,y">
<goal name="VC lrs.20.0.0" expl="postcondition" proved="true">
<transf name="instantiate" proved="true" arg1="Hinst" arg2="y">
<goal name="VC lrs.20.0.0.0" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
......
......@@ -1307,6 +1307,7 @@ qualid_comma_list_eof:
ident_comma_list_eof:
| comma_list1(ident) EOF { $1 }
(* TODO: Weird to not have any parser conflicts here *)
term_comma_list_eof:
| comma_list1(term) EOF { $1 }
| comma_list1(single_term) EOF { $1 }
(* we use single_term to avoid conflict with tuples, that
do not need parentheses *)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment