diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-10 20:37:37 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-10 20:37:37 +0000 |
| commit | e72024e2292a50684b7f280d6efb8fee090e2dbf (patch) | |
| tree | fdba2d8c55f0c74aee8800a0e8c9aec3d3b8a584 /kernel/instantiate.ml | |
| parent | 583992b6ce38655855f6625a26046ce84c53cdc1 (diff) | |
Suppression de Abst
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@593 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/instantiate.ml')
| -rw-r--r-- | kernel/instantiate.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml index 627f0d45c..9b1d9289a 100644 --- a/kernel/instantiate.ml +++ b/kernel/instantiate.ml @@ -72,7 +72,7 @@ let existential_value sigma (n,args) = | Evar_empty -> anomaly "a defined existential with no body" -let const_abst_opt_value env sigma c = +let const_evar_opt_value env sigma c = match c with | DOPN(Const sp,_) -> if evaluable_constant env c then Some (constant_value env c) else None @@ -81,7 +81,5 @@ let const_abst_opt_value env sigma c = Some (existential_value sigma (ev,args)) else None - | DOPN(Abst sp,_) -> - if evaluable_abst env c then Some (abst_value env c) else None | _ -> invalid_arg "const_abst_opt_value" |