First commit with new (incomplete) disambiguation engine.

[helm.git] / matitaB / components / grafite_parser / grafiteParser.ml

diff --git a/matitaB/components/grafite_parser/grafiteParser.ml b/matitaB/components/grafite_parser/grafiteParser.ml
index 492274f97ec50ff49196c271d24efdd949976bfd..2c9f44554ad00a2edce564643be7c11ab880f81c 100644 (file)
--- a/matitaB/components/grafite_parser/grafiteParser.ml
+++ b/matitaB/components/grafite_parser/grafiteParser.ml
@@ -59,7 +59,7 @@ let default_associativity = Gramext.NonA
 let mk_rec_corec ind_kind defs loc = 
   let name,ty = 
     match defs with
-    | (params,(N.Ident (name, None), ty),_,_) :: _ ->
+    | (params,(N.Ident (name, `Ambiguous), ty),_,_) :: _ ->
         let ty = match ty with Some ty -> ty | None -> N.Implicit `JustOne in
         let ty =
          List.fold_right
@@ -69,7 +69,7 @@ let mk_rec_corec ind_kind defs loc =
          name,ty
     | _ -> assert false 
   in
-  let body = N.Ident (name,None) in
+  let body = N.Ident (name,`Ambiguous) in
    (loc, N.Theorem(`Definition, name, ty, Some (N.LetRec (ind_kind, defs, body)), `Regular))
 
 let nmk_rec_corec ind_kind defs loc = 
@@ -430,6 +430,7 @@ EXTEND
         (params,name,typ,fields)
     ] ];
 
+    (* XXX: alias spec must be revised (no more instance nums) *)
     alias_spec: [
       [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
         let alpha = "[a-zA-Z]" in
@@ -455,14 +456,14 @@ EXTEND
           let instance =
             match instance with Some i -> i | None -> 0
           in
-          G.Symbol_alias (symbol, instance, dsc)
+          G.Symbol_alias (symbol, None, dsc)
       | IDENT "num";
         instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
         SYMBOL "="; dsc = QSTRING ->
           let instance =
             match instance with Some i -> i | None -> 0
           in
-          G.Number_alias (instance, dsc)
+          G.Number_alias (None,dsc)
       ]
      ];
     argument: [