From 5d4368413bdf9d8e670bab23b912994bc2f8459d Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 22 Apr 2004 13:54:12 +0000 Subject: [PATCH] added (and used) some type shorthands --- .../cic_disambiguation/cicTextualParser2.mli | 17 +++++------------ .../cic_disambiguation/disambiguateTypes.mli | 8 ++++++++ 2 files changed, 13 insertions(+), 12 deletions(-) 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 + -- 2.39.2