diff options
| author | herbelin | 1999-11-30 18:49:45 +0000 |
|---|---|---|
| committer | herbelin | 1999-11-30 18:49:45 +0000 |
| commit | 8b882c1ab5a31eea35eec89f134238dd17b945c2 (patch) | |
| tree | f5a287c1a839652f9dea8c8eeb6148a6e37b3da7 | |
| parent | 788402887777136c180a177ac41909b09727e159 (diff) | |
inductive_key et constructor_key
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@166 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/rawterm.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index f2df08842d..03d0d6e47e 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -11,12 +11,12 @@ open Type_errors type loc = int * int -type indtype_id = section_path * int -type constructor_id = indtype_id * int +type inductive_key = section_path * int +type constructor_key = inductive_key * int type pattern = (* locs here refers to the ident's location, not whole pat *) | PatVar of loc * name - | PatCstr of loc * (constructor_id * identifier list) * pattern list + | PatCstr of loc * (constructor_key * identifier list) * pattern list | PatAs of loc * identifier * pattern type binder_kind = BProd | BLambda @@ -25,8 +25,8 @@ type rawsort = RProp of Term.contents | RType type reference = | RConst of section_path * identifier list - | RInd of indtype_id * identifier list - | RConstruct of constructor_id * identifier list + | RInd of inductive_key * identifier list + | RConstruct of constructor_key * identifier list | RAbst of section_path | RVar of identifier | REVar of int * identifier list |