From: Stefano Zacchiroli Date: Thu, 22 Apr 2004 13:54:12 +0000 (+0000) Subject: added (and used) some type shorthands X-Git-Tag: dead_dir_walking~7 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=5d4368413bdf9d8e670bab23b912994bc2f8459d added (and used) some type shorthands --- diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli index e867d3435..e6b1ff7e1 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli @@ -25,20 +25,13 @@ exception Parse_error of string -(** {3 type shortands} *) - -type tactic = (CicAst.term, string) TacticAst.tactic -type tactical = (CicAst.term, string) TacticAst.tactic TacticAst.tactical -type command = CicAst.term CommandAst.command -type script = CicAst.term CommandAst.Script.script - (** {2 Parsing functions} *) -val parse_term: char Stream.t -> CicAst.term -val parse_tactic: char Stream.t -> tactic -val parse_tactical: char Stream.t -> tactical -val parse_command: char Stream.t -> command -val parse_script: char Stream.t -> script +val parse_term: char Stream.t -> DisambiguateTypes.term +val parse_tactic: char Stream.t -> DisambiguateTypes.tactic +val parse_tactical: char Stream.t -> DisambiguateTypes.tactical +val parse_command: char Stream.t -> DisambiguateTypes.command +val parse_script: char Stream.t -> DisambiguateTypes.script (** {2 Grammar extensions} *) diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli index 523fe4b70..58458d1ff 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli @@ -53,3 +53,11 @@ module type Callbacks = val string_of_domain_item: domain_item -> string val string_of_domain: domain_item list -> string +(** {3 type shortands} *) + +type term = CicAst.term +type tactic = (term, string) TacticAst.tactic +type tactical = (term, string) TacticAst.tactic TacticAst.tactical +type command = term CommandAst.command +type script = term CommandAst.Script.script +