diff options
| author | barras | 2001-05-23 15:13:07 +0000 |
|---|---|---|
| committer | barras | 2001-05-23 15:13:07 +0000 |
| commit | dc2e676c9cdedea43805c21a4b3203832a985f95 (patch) | |
| tree | 849760ef13d1460d603ce9436c244922e13a6080 /kernel/reduction.mli | |
| parent | a023ff2e48aaf7ebfb15e10dc7cdb80ab2991e8e (diff) | |
amelioration des messages d'erreurs vis a vis des evars
ajout automatique des chemins vers les sources au moment du Drop
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 15 |
1 files changed, 2 insertions, 13 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index ae0640aef0..a32f36a6af 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -58,8 +58,8 @@ val stacklam : (state -> 'a) -> constr list -> constr -> constr stack -> 'a val clos_norm_flags : Closure.flags -> 'a reduction_function (* Same as [(strong whd_beta[delta][iota])], but much faster on big terms *) -val nf_beta : 'a reduction_function -val nf_betaiota : 'a reduction_function +val nf_beta : local_reduction_function +val nf_betaiota : local_reduction_function val nf_betadeltaiota : 'a reduction_function (* Lazy strategy, weak head reduction *) @@ -101,7 +101,6 @@ val whd_betadeltaeta : 'a reduction_function val whd_betadeltaiotaeta_stack : 'a stack_reduction_function val whd_betadeltaiotaeta_state : 'a state_reduction_function val whd_betadeltaiotaeta : 'a reduction_function -val whd_evar : 'a reduction_function val beta_applist : constr * constr list -> constr @@ -192,16 +191,6 @@ val whd_meta : (int * constr) list -> constr -> constr val plain_instance : (int * constr) list -> constr -> constr val instance : (int * constr) list -> constr -> constr -(* [whd_ise] raise [Uninstantiated_evar] if an evar remains uninstantiated; *) -(* *[whd_ise1]* is synonymous of *[whd_evar empty_env]* and *[nf_ise1]* of *) -(* *[strong whd_evar empty_env]*: they leave uninstantiated evar as it *) - -val whd_ise1 : 'a evar_map -> constr -> constr -val nf_ise1 : 'a evar_map -> constr -> constr -exception Uninstantiated_evar of int -val whd_ise : 'a evar_map -> constr -> constr -val whd_castappevar : 'a evar_map -> constr -> constr - (*s Obsolete Reduction Functions *) (*i |