Exists is no longer an ad-hoc notation hard-coded in the parser.

[helm.git] / helm / software / components / content_pres / cicNotationParser.ml

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 8940c6614ebafb0622fb6bc83f348e88eb40854b..d7da2ff822d27f46a817820a11db23caf6ccd888 100644 (file)
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -150,6 +150,7 @@ let extract_term_production pattern =
     | Ast.Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\below"] @ aux p2
     | Ast.Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\above"] @ aux p2
     | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac"] @ aux p2
+    | Ast.InfRule (p1, p2, p3) -> aux p1 @ [NoBinding, gram_symbol "\\infrule"] @ aux p2 @ aux p3
     | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop"] @ aux p2
     | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over"] @ aux p2
     | Ast.Root (p1, p2) ->
@@ -233,6 +234,7 @@ let check_l1_pattern level1_pattern level associativity =
     | Ast.Below (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Below (p1, p2)
     | Ast.Above (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Above (p1, p2)
     | Ast.Frac (p1, p2)  -> let p1 = aux p1 in let p2 = aux p2 in Ast.Frac (p1, p2)
+    | Ast.InfRule (p1, p2, p3)  -> let p1 = aux p1 in let p2 = aux p2 in let p3 = aux p3 in Ast.InfRule (p1, p2, p3)
     | Ast.Atop (p1, p2)  -> let p1 = aux p1 in let p2 = aux p2 in Ast.Atop (p1, p2)
     | Ast.Over (p1, p2)  -> let p1 = aux p1 in let p2 = aux p2 in Ast.Over (p1, p2)
     | Ast.Root (p1, p2)  -> let p1 = aux p1 in let p2 = aux p2 in Ast.Root (p1, p2)
@@ -426,6 +428,9 @@ EXTEND
       | SYMBOL "\\frac"; p1 = SELF; p2 = SELF ->
           return_term_of_level loc 
             (fun l -> Ast.Layout (Ast.Frac (p1 l, p2 l)))
+      | SYMBOL "\\infrule"; p1 = SELF; p2 = SELF; p3 = SELF ->
+          return_term_of_level loc 
+            (fun l -> Ast.Layout (Ast.InfRule (p1 l, p2 l, p3 l)))
       | SYMBOL "\\sqrt"; p = SELF -> 
           return_term_of_level loc (fun l -> Ast.Layout (Ast.Sqrt p l))
       | SYMBOL "\\root"; index = SELF; SYMBOL "\\of"; arg = SELF ->
@@ -545,7 +550,6 @@ EXTEND
   ];
   binder: [
     [ SYMBOL <:unicode<Pi>>     (* Π *) -> `Pi
-(*     | SYMBOL <:unicode<exists>> |+ ∃ +| -> `Exists *)
     | SYMBOL <:unicode<forall>> (* ∀ *) -> `Forall
     | SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
     ]
@@ -644,9 +648,6 @@ EXTEND
     [
       [ b = binder; (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19" ->
           return_term loc (fold_cluster b vars typ body)
-      | SYMBOL <:unicode<exists>> (* ∃ *);
-        (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19"->
-          return_term loc (fold_exists vars typ body)
       ]
     ];
   term: LEVEL "70"