Aliases definition removed from the

diff --git a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll
index d9b353cd708164258ac4822074a09b7444f756a3..58e6cf35b12d877e6fe61a2e251d6b3a5d34e7ca 100644 (file)
--- a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll
+++ b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll
@@ -60,7 +60,6 @@ let blanks = [' ' '\t' '\n']
 rule token =
  parse
     blanks      { token lexbuf } (* skip blanks *)
-  | "alias"     { ALIAS }
   | "Case"      { CASE }
   | "Fix"       { FIX }
   | "CoFix"     { COFIX }

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))
-    }

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml b/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml
index c51346e1ac3940625b7866df6bb7f0d6a3a77e01..6901bd48c28317c262a5444590e31f60cffdf83a 100644 (file)
--- a/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml
+++ b/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml
@@ -23,18 +23,14 @@
  * http://cs.unibo.it/helm/.
  *)
 
-let main ~context ~metasenv lexer lexbuf ~register_aliases =
+let main ~context ~metasenv lexer lexbuf =
  (* Warning: higly non-reentrant code!!! *)
  CicTextualParser0.binders := context ;
  CicTextualParser0.metasenv := metasenv ;
- match CicTextualParser.main lexer lexbuf register_aliases with
-    None -> None
-  | Some (dom,mk_term) ->
-     Some
-      (dom,
-        function interp ->
-         let term = mk_term interp in 
-         let metasenv = !CicTextualParser0.metasenv in
-          metasenv,term
-      )
+ let dom,mk_term = CicTextualParser.main lexer lexbuf in
+  dom,
+   function interp ->
+    let term = mk_term interp in 
+    let metasenv = !CicTextualParser0.metasenv in
+     metasenv,term
 ;;

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli b/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli
index 23ad4af115ef8edd9205c1a2298d4db3dd81aec3..c83ac03f8b1df4beeb2cfccfa3dad241ecf69cae 100644 (file)
--- a/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli
+++ b/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli
@@ -27,7 +27,5 @@ val main :
   context:((Cic.name option) list) ->
   metasenv:Cic.metasenv ->
   (Lexing.lexbuf  -> CicTextualParser.token) -> Lexing.lexbuf ->
-  register_aliases:((string * CicTextualParser0.uri) -> unit) ->
-   (string list *
+   string list *
     ((string -> CicTextualParser0.uri option) -> (Cic.metasenv * Cic.term))
-   ) option