Souci avec example fbidon...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2888 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 2 deletions

diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 2215492a3..86de23302 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