From 8301010603574301ec56728727093ad456cd12ad Mon Sep 17 00:00:00 2001
From: barras
Date: Thu, 29 Jul 2010 15:23:32 +0000
Subject: fixed bug #2105 (compilation of free de Bruijn) and missing lift of
 predicate in branch read-back

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13349 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/cbytegen.ml  | 2 +-
 kernel/csymtable.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 26e76d6947..cdbd827baf 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -197,7 +197,7 @@ let pos_rel i r sz =
     let i = i - r.nb_stack in
     if i <= r.nb_rec then
       try List.nth r.pos_rec (i-1)
-      with _ -> assert false
+      with (Failure _|Invalid_argument _) -> assert false
     else
       let i = i - r.nb_rec in
       let db = FVrel(i) in
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 5e78e71de3..77a322905c 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -160,7 +160,7 @@ and slot_for_fv env fv =
 	    let (_, b, _) = lookup_rel i env.env_rel_context in
 	    let (v, d) =
 	      match b with
-		| None -> (val_of_rel i, Idset.empty)
+		| None -> (val_of_rel (nb_rel env - i), Idset.empty)
 		| Some c -> let renv =  env_of_rel i env in
 			      (val_of_constr renv c, Environ.global_vars_set (Environ.env_of_pre_env renv) c)
 	    in
-- 
cgit v1.2.3