%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
-%token PLUS MINUS TIMES EQT EQ
+%token PLUS MINUS TIMES EQT EQ NEQT
%right ARROW
-%right EQ EQT
-%right PLUS MINUS RPLUS RMINUS
-%right TIMES RTIMES RDIV
+%nonassoc EQ EQT NEQT
+%left PLUS MINUS RPLUS RMINUS
+%left TIMES RTIMES RDIV
%start main
%type <CicTextualParser0.interpretation_domain_item list * (CicTextualParser0.interpretation -> Cic.term)> main
%%
(mk_expr2 interp)
]
}
+ | expr2 NEQT expr2
+ { let dom1,mk_expr1 = $1 in
+ let dom2,mk_expr2 = $3 in
+ let dom3,mk_expr3 = mk_implicit () in
+ let dom = union dom1 (union dom2 dom3) in
+ dom, function interp ->
+ Cic.Appl [
+ Cic.Const (UriManager.uri_of_string "cic:/Coq/Init/Logic/not.con",[]);
+ Cic.Appl
+ [Cic.MutInd
+ (UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind",0,[]) ;
+ (mk_expr3 interp) ;
+ (mk_expr1 interp) ;
+ (mk_expr2 interp)
+ ]]
+ }
| expr2 EQ expr2
{ let dom1,mk_expr1 = $1 in
let dom2,mk_expr2 = $3 in
}
| 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