From 1d758eca0ab5524a4f24aaa41425716c52618e0c Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 16 Jul 2002 15:33:27 +0000
Subject: Souci avec example fbidon...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2888 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/mlutil.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 2215492a32..86de23302b 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -196,7 +196,7 @@ let rec ml_subst e =
   in subst 0
 
 (*s Generalized substitution. 
-   [gensubst v m d t] applies to [t] the substitution coded in the 
+   [gen_subst v m d t] applies to [t] the substitution coded in the 
    [v] array: [(Rel i)] becomes [(Rel v.(i))]. [d] is the correction applies 
    to [Rel] greater than [m]. *)
 
@@ -205,7 +205,9 @@ let gen_subst v d t =
     | MLrel i as a -> 
 	let i'= i-n in 
 	if i' < 1 then a 
-	else if i' < Array.length v then MLrel (v.(i')+n) 
+	else if i' < Array.length v then 
+	  if v.(i') = 0 then MLdummy
+	  else MLrel (v.(i')+n) 
 	else MLrel (i+d) 
     | a -> ast_map_lift subst n a
   in subst 0 t
-- 
cgit v1.2.3