X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationEnv.ml;h=9a4a8e20b8ad0e57fdc101f49b20479d412da33c;hb=1946ca7a51df0acb35d8e2ea001d194f1d2ccb12;hp=f914b01d2ea57df51689ee1c5c76281dc8208cdb;hpb=ea7808d83a7d6e03c0e163f0691e268dcd7c2ea4;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationEnv.ml b/helm/ocaml/cic_notation/cicNotationEnv.ml index f914b01d2..9a4a8e20b 100644 --- a/helm/ocaml/cic_notation/cicNotationEnv.ml +++ b/helm/ocaml/cic_notation/cicNotationEnv.ml @@ -23,10 +23,10 @@ * http://helm.cs.unibo.it/ *) -open CicNotationPt +module Ast = CicNotationPt type value = - | TermValue of term + | TermValue of Ast.term | StringValue of string | NumValue of string | OptValue of value option @@ -94,19 +94,19 @@ let opt_declaration (n, ty) = (n, OptType ty) let list_declaration (n, ty) = (n, ListType ty) let declaration_of_var = function - | NumVar s -> s, NumType - | IdentVar s -> s, StringType - | TermVar s -> s, TermType + | Ast.NumVar s -> s, NumType + | Ast.IdentVar s -> s, StringType + | Ast.TermVar s -> s, TermType | _ -> assert false let value_of_term = function - | Num (s, _) -> NumValue s - | Ident (s, None) -> StringValue s + | Ast.Num (s, _) -> NumValue s + | Ast.Ident (s, None) -> StringValue s | t -> TermValue t let term_of_value = function - | NumValue s -> Num (s, 0) - | StringValue s -> Ident (s, None) + | NumValue s -> Ast.Num (s, 0) + | StringValue s -> Ast.Ident (s, None) | TermValue t -> t | _ -> assert false (* TO BE UNDERSTOOD *)