From 351c92f5c61082e9e8f5e1c9364f1836416f17d3 Mon Sep 17 00:00:00 2001 From: mdenes Date: Mon, 11 Feb 2013 09:45:49 +0000 Subject: Fixing bug in native compiler with let patterns in fixpoint definitions. Typical example: Fixpoint f (m : nat) (o := true) (n : nat) {struct n} := n. Was raising an "index out of bounds" exception at compile-time. Nota: this construction is still incorrectly handled by the VM. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16197 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/nativelambda.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'kernel/nativelambda.mli') diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 0c454256e..ada63ebb4 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -46,6 +46,7 @@ and lam_branches = (constructor * name array * lambda) array and fix_decl = name array * lambda array * lambda array val decompose_Llam : lambda -> Names.name array * lambda +val decompose_Llam_Llet : lambda -> (Names.name * lambda option) array * lambda val is_lazy : constr -> bool val mk_lazy : lambda -> lambda -- cgit v1.2.3