%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT NONE
%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
%token DOLLAR
-%token PLUS TIMES EQ
+%token PLUS MINUS TIMES EQ
%right ARROW
%right EQ
-%right PLUS
+%right PLUS MINUS
%right TIMES
%start main
%type <CicTextualParser0.interpretation_domain_item list * (CicTextualParser0.interpretation -> Cic.term)> main
(mk_expr2 interp)
]
}
+ | expr2 MINUS expr2
+ { let dom1,mk_expr1 = $1 in
+ let dom2,mk_expr2 = $3 in
+ let dom = union dom1 dom2 in
+ dom, function interp ->
+ Cic.Appl
+ [Cic.Const
+ (UriManager.uri_of_string "cic:/Coq/Arith/Minus/minus.con",[]) ;
+ (mk_expr1 interp) ;
+ (mk_expr2 interp)
+ ]
+ }
| expr2 TIMES expr2
{ let dom1,mk_expr1 = $1 in
let dom2,mk_expr2 = $3 in