divers

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

2 files changed, 9 insertions, 6 deletions

diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 31c68e025e..89dcd07c5a 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -62,7 +62,7 @@ let rec ast_map f = function
   | MLfix (fi,ids,al) -> MLfix (fi, ids, List.map f al)
   | MLcast (a,t) -> MLcast (f a, t)
   | MLmagic a -> MLmagic (f a)
-  | a -> a
+  | MLrel _ | MLglob _ | MLexn _ | MLprop | MLarity as a -> a
 
 and ast_map_eqn f (c,ids,a) = (c,ids,f a)
 
@@ -99,11 +99,11 @@ let ml_pop c = ml_lift (-1) c
 
 let rec ml_subst v =
   let rec subst n m = function
-    | MLrel i ->
+    | MLrel i as a ->
 	if i = n then
 	  m
 	else 
-	  if i < n then MLrel i else MLrel (i-1)
+	  if i < n then a else MLrel (i-1)
     | MLlam (id,t) ->
 	MLlam (id, subst (n+1) (ml_lift 1 m) t)
     | MLletin (id,a,b) ->
@@ -117,7 +117,8 @@ let rec ml_subst v =
 	MLfix (i,ids, 
 	       let k = List.length ids in
 	       List.map (subst (n+k) (ml_lift k m)) cl)
-    | a -> ast_map (subst n m) a
+    | a -> 
+	ast_map (subst n m) a
   in 
   subst 1 v
 
@@ -178,7 +179,7 @@ let rec betaiota = function
 	 | MLlam (id,t) -> 
 	     (match nb_occur t with
 		| 0 -> betaiota (MLapp (ml_pop t, List.tl a'))
-		| 1 -> betaiota (MLapp (ml_subst (List.hd a') t,List.tl a'))
+		| 1 -> betaiota (MLapp (ml_subst (List.hd a') t, List.tl a'))
 		| _ -> betaiota (MLletin (id, List.hd a', 
 					  MLapp (t, List.tl a'))))
 	 (* application of a let in: we push arguments inside *)
@@ -207,7 +208,7 @@ let rec betaiota = function
 	     betaiota (MLapp (c',a))
 	 | e' -> 
 	     MLcase (e', Array.map (fun (n,l,t) -> (n,l,betaiota t)) br))
-  | MLletin(i,c,e) when (is_atomic c) || (nb_occur e <= 1) -> 
+  | MLletin(_,c,e) when (is_atomic c) || (nb_occur e <= 1) -> 
       betaiota (ml_subst c e)
   | a -> 
       ast_map betaiota a
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index 0602567cb7..332a34e6cf 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -33,6 +33,8 @@ val ml_lift : int -> ml_ast -> ml_ast
 
 val ml_subst : ml_ast -> ml_ast -> ml_ast
 
+val subst_glob_ast : global_reference -> ml_ast -> ml_ast -> ml_ast
+
 (*s Some transformations of ML terms. [normalize] and [normalize_decl] reduce
     all beta redexes (when the argument does not occur, it is just
     thrown away; when it occurs exactly once it is substituted; otherwise