Commit 85509592 authored by Robbert Krebbers's avatar Robbert Krebbers

Correctly coerce `ident` into `spec_pat` in `spec_pat.parse`.

This became broken after the nested iSpecialize MR.
parent 12db2bda
......@@ -95,7 +95,7 @@ Ltac parse s :=
| string => lazymatch eval vm_compute in (parse s) with
| Some ?pats => pats | _ => fail "spec_pat.parse: cannot parse" s
end
| ident => constr:([SIdent s])
| ident => constr:([SIdent s []])
| ?X => fail "spec_pat.parse:" s "has unexpected type" X
end.
End spec_pat.
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