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.ml | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'kernel/nativelambda.ml')

diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 2ca2747994..f530f6e2ec 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -66,6 +66,20 @@ let decompose_Llam lam =
   | Llam(ids,body) -> ids, body
   | _ -> [||], lam
 
+let rec decompose_Llam_Llet lam =
+  match lam with
+  | Llam(ids,body) ->
+      let vars, body = decompose_Llam_Llet body in
+      Array.fold_right (fun x l -> (x, None) :: l) ids vars, body
+  | Llet(id,def,body) ->
+      let vars, body = decompose_Llam_Llet body in
+      (id,Some def) :: vars, body
+  | _ -> [], lam
+
+let decompose_Llam_Llet lam =
+  let vars, body = decompose_Llam_Llet lam in
+  Array.of_list vars, body
+
 (*s Operators on substitution *)
 let subst_id = subs_id 0
 let lift = subs_lift 
-- 
cgit v1.2.3