prima implementazione di demodulate, superposition_left e superposition_right

[helm.git] / helm / ocaml / cic_notation / cicNotationParser.ml

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index ea66d6af42f7a747388e423729c65e1025d18879..6bc494cdc5801be74a740972c16abf665dd60c9d 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -244,10 +244,6 @@ let delete atoms = Grammar.delete_rule l2_pattern atoms
 
 (** {2 Grammar} *)
 
-let boxify = function
-  | [ a ] -> a
-  | l -> Layout (Box (H, l))
-
 let fold_binder binder pt_names body =
   let fold_cluster binder terms ty body =
     List.fold_right
@@ -329,7 +325,7 @@ EXTEND
           return_term loc (Layout (Box (V, p)))
       | SYMBOL "\\BREAK" -> return_term loc (Layout Break)
       | DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
-          return_term loc (boxify p)
+          return_term loc (CicNotationUtil.boxify p)
       | p = SELF; SYMBOL "\\AS"; id = IDENT ->
           return_term loc (Variable (Ascription (p, id)))
       ]
@@ -525,15 +521,15 @@ EXTEND
 (* }}} *)
 (* {{{ Grammar for interpretation, notation level 3 *)
   argument: [
-    [ id = IDENT -> IdentArg id
-    | SYMBOL <:unicode<eta>> (* η *); SYMBOL "."; a = SELF -> EtaArg (None, a)
-    | SYMBOL <:unicode<eta>> (* η *); id = IDENT; SYMBOL "."; a = SELF ->
-        EtaArg (Some id, a)
+    [ id = IDENT -> IdentArg (0, id)
+    | l = LIST1 [ SYMBOL <:unicode<eta>> (* η *) -> () ] SEP SYMBOL ".";
+      SYMBOL "."; id = IDENT ->
+        IdentArg (List.length l, id)
     ]
   ];
   level3_term: [
     [ u = URI -> UriPattern u
-    | a = argument -> ArgPattern a
+    | id = IDENT -> VarPattern id
     | SYMBOL "("; terms = LIST1 SELF; SYMBOL ")" ->
         (match terms with
         | [] -> assert false