X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_textual_parser%2FcicTextualParser.mly;h=9fd6ec52a1ec62c9c24991bc1f91f1a4ebc337ea;hb=9d35b4005007408a49a76864302f03db8aa7789a;hp=dcb77c701429ded6671ff0e5076d90b718117e97;hpb=71b08b1ea99893b3c5e2d91fc26e1ab7330fd33d;p=helm.git

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
index dcb77c701..9fd6ec52a 100644
--- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
@@ -144,12 +144,10 @@
 %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
 %right ARROW
 %start main
-%type <((string * CicTextualParser0.uri) -> unit) -> (string list * ((string -> CicTextualParser0.uri option) -> Cic.term)) option> main
+%type <string list * ((string -> CicTextualParser0.uri option) -> Cic.term)> main
 %%
 main:
-   expr  { function _ -> Some $1 }
- | alias { function register -> register $1 ; None }
- | EOF   { raise CicTextualParser0.Eof }
+ expr EOF { $1 }
 ;
 expr2:
    CONURI exp_named_subst
@@ -479,15 +477,3 @@ substitutionlist:
     { let dom,mk_exprsubstitutionlist = $3 in
        dom, function interp -> None::(mk_exprsubstitutionlist interp)
     }
-;
-alias:
-   ALIAS ID CONURI
-    { $2,(CicTextualParser0.ConUri $3) }
- | ALIAS ID VARURI
-    { $2,(CicTextualParser0.VarUri $3) }
- | ALIAS ID INDTYURI
-    { $2,(CicTextualParser0.IndTyUri (fst $3, snd $3)) }
- | ALIAS ID INDCONURI
-    { let uri,indno,consno = $3 in
-       $2,(CicTextualParser0.IndConUri (uri, indno, consno))
-    }