X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftex_cic_textual_parser%2FtexCicTextualParser.mly;h=f6f557947a0598509c1ce9c45f66fc0f79b99009;hb=b38de2d3fa8bbe346c59c18bbeb889f29e493f63;hp=500565823d20a328166fd06dda7e2222d4860777;hpb=a335fa89b0340ba3fb5d60566075ca83b5bda5d1;p=helm.git

diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
index 500565823..f6f557947 100644
--- a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
+++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
@@ -156,7 +156,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
 %token DOLLAR
 %token RPLUS RMINUS RTIMES RDIV
@@ -473,9 +473,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