From a99d872330dd1ddb5248528c06a2c97aeafb5a59 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 2 Feb 2004 16:44:26 +0000 Subject: [PATCH] - added capture_variable entry and Cic.names here and there --- .../cic_disambiguation/cicTextualParser2Ast.mli | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2Ast.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2Ast.mli index b7267ee57..1b5933f7d 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2Ast.mli +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2Ast.mli @@ -31,7 +31,7 @@ type ('term, 'ident) tactic = | Injection of 'ident | Intros of int option | Left - | LetIn of 'term * 'ident + | LetIn of 'term * 'ident (* TODO clashes with term below *) | Named_intros of 'ident list | Reduce of reduction_kind * 'term pattern * 'ident option (* what, where *) | Reflexivity @@ -63,27 +63,26 @@ type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ] type induction_kind = [ `Inductive | `CoInductive ] type sort_kind = [ `Prop | `Set | `Type | `CProp ] -type case_pattern = string list - type term = | LocatedTerm of location * term | Appl of term list - | Appl_symbol of string * int * term list (* literal, args, instance *) - | Binder of binder_kind * Cic.name * term option * term - (* kind, name, type, body *) + | Appl_symbol of string * int * term list (* literal, instance, args *) + | Binder of binder_kind * capture_variable * term (* kind, name, body *) | Case of term * string * term option * (case_pattern * term) list (* what to match, inductive type, out type, list *) - | LetIn of string * term * term (* name, body, where *) - | LetRec of induction_kind * (string * term * term option * int) list * term - (* (name, body, type, decreasing argument) list, where *) + | LetIn of capture_variable * term * term (* name, body, where *) + | LetRec of induction_kind * (capture_variable * term * int) list * term + (* (name, body, decreasing argument) list, where *) | Ident of string * subst list (* literal, substitutions *) | Meta of int * meta_subst list | Num of string * int (* literal, instance *) | Sort of sort_kind +and capture_variable = Cic.name * term option (* name, type *) and meta_subst = term option and subst = string * term +and case_pattern = string * capture_variable list (* type cexpr = -- 2.39.2