diff options
| author | herbelin | 2001-02-07 10:02:40 +0000 |
|---|---|---|
| committer | herbelin | 2001-02-07 10:02:40 +0000 |
| commit | 78384438637eb9ce2f11f61bafc59f17c5f933da (patch) | |
| tree | f1968f737066e0e736f01b5fd4c8c9c5bccacdfc /kernel/term.mli | |
| parent | 9c662cf9e8f4065ab354dc9c55c3e819f0db1fbe (diff) | |
Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1340 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index e3f6b44635..08b1e5e863 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -39,7 +39,6 @@ type global_reference = | ConstRef of constant_path | IndRef of inductive_path | ConstructRef of constructor_path - | EvarRef of int (********************************************************************) (* The type of constructions *) @@ -79,7 +78,7 @@ type arity = rel_declaration list * sorts (* [constr array] is an instance matching definitional [named_context] in the same order (i.e. last argument first) *) -type existential = int * constr array +type existential = existential_key * constr array type constant = constant_path * constr array type constructor = constructor_path * constr array type inductive = inductive_path * constr array @@ -314,8 +313,8 @@ val path_of_const : constr -> constant_path val args_of_const : constr -> constr array (* Destructs an existential variable *) -val destEvar : constr -> int * constr array -val num_of_evar : constr -> int +val destEvar : constr -> existential_key * constr array +val num_of_evar : constr -> existential_key (* Destructs a (co)inductive type *) val destMutInd : constr -> inductive |