diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-07 10:02:40 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-07 10:02:40 +0000 |
| commit | 78384438637eb9ce2f11f61bafc59f17c5f933da (patch) | |
| tree | f1968f737066e0e736f01b5fd4c8c9c5bccacdfc /kernel | |
| 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')
| -rw-r--r-- | kernel/environ.ml | 2 | ||||
| -rw-r--r-- | kernel/term.ml | 1 | ||||
| -rw-r--r-- | kernel/term.mli | 7 |
3 files changed, 3 insertions, 7 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 287cff598..0c51f085e 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -219,8 +219,6 @@ let sp_of_global env = function let mip = mind_nth_type_packet mib tyi in assert (i <= Array.length mip.mind_consnames && i > 0); make_path (dirpath sp) mip.mind_consnames.(i-1) CCI - | EvarRef n -> - make_path [] (id_of_string ("?"^(string_of_int n))) CCI let id_of_global env ref = basename (sp_of_global env ref) diff --git a/kernel/term.ml b/kernel/term.ml index ee98a7054..7503aa03a 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -44,7 +44,6 @@ type global_reference = | ConstRef of constant_path | IndRef of inductive_path | ConstructRef of constructor_path - | EvarRef of int (********************************************************************) (* Constructions as implemented *) diff --git a/kernel/term.mli b/kernel/term.mli index e3f6b4463..08b1e5e86 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 |