diff options
| author | ppedrot | 2013-10-29 19:47:14 +0000 |
|---|---|---|
| committer | ppedrot | 2013-10-29 19:47:14 +0000 |
| commit | 943b5f9a9a90e856171f9dcb13ae56eaa8d87ef0 (patch) | |
| tree | 366dd6d33017f7f00f99ede753585be989f5a9ce /pretyping/reductionops.mli | |
| parent | b8098068f29a58a478efa719c51271d09f66a9d8 (diff) | |
Do not generate useless argument arrays in whd_* functions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16954 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index b98a7d3095..6640392063 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -115,6 +115,7 @@ val nf_betaiota_preserving_vm_cast : reduction_function (** Lazy strategy, weak head reduction *) val whd_evar : evar_map -> constr -> constr +val whd_nored : local_reduction_function val whd_beta : local_reduction_function val whd_betaiota : local_reduction_function val whd_betaiotazeta : local_reduction_function |