diff options
| -rw-r--r-- | dev/base_include | 3 | ||||
| -rw-r--r-- | parsing/g_constr.ml4 | 2 |
2 files changed, 3 insertions, 2 deletions
diff --git a/dev/base_include b/dev/base_include index 26949cde98..829c5ea61c 100644 --- a/dev/base_include +++ b/dev/base_include @@ -64,9 +64,10 @@ open Pattern open Cbv open Classops open Pretyping +open Pretyping.Default +open Pretyping.Default.Cases open Cbv open Classops -open Pretyping open Clenv open Rawterm open Coercion diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 5e68c73089..10d7f46b57 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -275,7 +275,7 @@ GEXTEND Gram [ [ OPT"|"; br=LIST0 eqn SEP "|" -> br ] ] ; eqn: - [ [ pll = LIST0 LIST1 pattern LEVEL "99" SEP "," SEP "|"; + [ [ pll = LIST1 LIST1 pattern LEVEL "99" SEP "," SEP "|"; "=>"; rhs = lconstr -> (loc,pll,rhs) ] ] ; pattern: |