From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- checker/reduction.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'checker/reduction.mli') diff --git a/checker/reduction.mli b/checker/reduction.mli index 2f551f4a..15a2df1f 100644 --- a/checker/reduction.mli +++ b/checker/reduction.mli @@ -16,8 +16,8 @@ open Environ (*s Reduction functions *) val whd_betaiotazeta : constr -> constr -val whd_betadeltaiota : env -> constr -> constr -val whd_betadeltaiota_nolet : env -> constr -> constr +val whd_all : env -> constr -> constr +val whd_allnolet : env -> constr -> constr (************************************************************************) (*s conversion functions *) -- cgit v1.2.3