From d6898781f9cd52ac36a4891d7b169ddab7b8af50 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Tue, 2 May 2017 19:53:05 +0200 Subject: Correct coqchk reduction --- checker/closure.mli | 3 +++ 1 file changed, 3 insertions(+) (limited to 'checker/closure.mli') diff --git a/checker/closure.mli b/checker/closure.mli index 8b1f246c2..8da9ad4ea 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -125,6 +125,9 @@ type stack_member = and stack = stack_member list val append_stack : fconstr array -> stack -> stack + +val stack_args_size : stack -> int + val eta_expand_stack : stack -> stack val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> -- cgit v1.2.3