removed dependency on netclient, use http_client module from ocaml-http

[helm.git] / helm / ocaml / tex_cic_textual_parser / texCicTextualParser.mly

diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
index f5aa714172cfe3328e530ab387c8d6a2ffb3f626..f6f557947a0598509c1ce9c45f66fc0f79b99009 100644 (file)
--- a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
+++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
@@ -156,15 +156,15 @@
 %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
 %%
@@ -323,6 +323,22 @@ expr2:
           (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
@@ -457,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