From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 5 Sep 2003 16:22:09 +0000 (+0000)
Subject: added \neqt macro
X-Git-Tag: v0_0_1~28
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a335fa89b0340ba3fb5d60566075ca83b5bda5d1;p=helm.git

added \neqt macro
---

diff --git a/helm/gTopLevel/dictionary-cic.xml b/helm/gTopLevel/dictionary-cic.xml
index 9b5441679..1d63dac83 100644
--- a/helm/gTopLevel/dictionary-cic.xml
+++ b/helm/gTopLevel/dictionary-cic.xml
@@ -35,5 +35,6 @@
   <entry name="Type" class="i" val="Type"/>
 
   <entry name="eqt"  class="o" val="="/>
+  <entry name="neqt" class="o" val="&#x2260;"/>
 
 </dictionary>
diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
index 06bbab076..f6eda1ac8 100644
--- a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
+++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
@@ -114,6 +114,7 @@ rule token =
   | "\\pi"      { PROD }
   | "\\forall"  { PROD }
   | "\\eqt"     { EQT }
+  | "\\neqt"    { NEQT }
   | ':'         { COLON }
   | '.'         { DOT }
   | "\\to"      { ARROW }
diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
index 709e23f18..500565823 100644
--- a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
+++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
@@ -160,9 +160,9 @@
 %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
-%nonassoc EQ EQT
+%nonassoc EQ EQT NEQT
 %left PLUS MINUS RPLUS RMINUS
 %left TIMES RTIMES RDIV
 %start 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