Interface improvement (???): the Check button has been moved to a brand new

[helm.git] / helm / ocaml / cic_textual_parser / cicTextualParser.mly

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
index dcb77c701429ded6671ff0e5076d90b718117e97..9fd6ec52a1ec62c9c24991bc1f91f1a4ebc337ea 100644 (file)
--- 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))
-    }