diff options
Diffstat (limited to 'parsing/pattern.mli')
| -rw-r--r-- | parsing/pattern.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/parsing/pattern.mli b/parsing/pattern.mli index ba8a883a8a..41ac6108ac 100644 --- a/parsing/pattern.mli +++ b/parsing/pattern.mli @@ -9,7 +9,8 @@ open Environ (*i*) type constr_pattern = - | PRef of constr array Rawterm.reference + | PRef of global_reference + | PVar of identifier | PRel of int | PApp of constr_pattern * constr_pattern array | PSoApp of int * constr_pattern list @@ -25,6 +26,7 @@ type constr_label = | IndNode of inductive_path | CstrNode of constructor_path | VarNode of identifier + | SectionVarNode of section_path exception BoundPattern |