sort CProp added

[helm.git] / helm / ocaml / cic_textual_parser / cicTextualParser.mly

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
index 08d85a595a2b03c358f07586ffdd4eb86ab5c30a..84e0f0ee50bcc4f90808fac592323016252e8863 100644 (file)
--- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
@@ -155,7 +155,7 @@
 %token <UriManager.uri> VARURI
 %token <UriManager.uri * int> INDTYURI
 %token <UriManager.uri * int * int> INDCONURI
-%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT NONE
+%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CPROP CAST IMPLICIT NONE
 %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
 %right ARROW
 %start main
@@ -286,9 +286,10 @@ expr2:
     }
  | IMPLICIT
     { mk_implicit () }
- | SET  { [], function _ -> Sort Set }
- | PROP { [], function _ -> Sort Prop }
- | TYPE { [], function _ -> Sort Type }
+ | SET   { [], function _ -> Sort Set }
+ | PROP  { [], function _ -> Sort Prop }
+ | TYPE  { [], function _ -> Sort Type }
+ | CPROP { [], function _ -> Sort CProp }
  | LPAREN expr CAST expr RPAREN
     { let dom1,mk_expr1 = $2 in
       let dom2,mk_expr2 = $4 in