From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 18 Nov 2002 14:37:09 +0000 (+0000)
Subject: Aliases definition removed from the
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4d60b73b5381a326afe3fe6a095dbe9dba68ed64;p=helm.git

Aliases definition removed from the
---

diff --git a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll
index d9b353cd7..58e6cf35b 100644
--- 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 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))
-    }
diff --git a/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml b/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml
index c51346e1a..6901bd48c 100644
--- 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 23ad4af11..c83ac03f8 100644
--- 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