From 3b03eb1015f14e04e505b11c27fb38b7db6ebe87 Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 9 May 2006 21:15:07 +0000
Subject: subst. explicites avec vecteurs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8799 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/term.ml | 22 ++++++++++------------
 1 file changed, 10 insertions(+), 12 deletions(-)

(limited to 'kernel/term.ml')

diff --git a/kernel/term.ml b/kernel/term.ml
index b082c091ef..87c319a1bf 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -752,19 +752,17 @@ let rec lift_substituend depth s =
 
 let make_substituend c = { sinfo=Unknown; sit=c }
 
-let substn_many lamv n =
+let substn_many lamv n c =
   let lv = Array.length lamv in 
-  let rec substrec depth c = match kind_of_term c with
-    | Rel k     ->
-        if k<=depth then 
-	  c
-        else if k-depth <= lv then
-          lift_substituend depth lamv.(k-depth-1)
-        else 
-	  mkRel (k-lv)
-    | _ -> map_constr_with_binders succ substrec depth c
-  in 
-  substrec n
+  if lv = 0 then c
+  else 
+    let rec substrec depth c = match kind_of_term c with
+      | Rel k     ->
+          if k<=depth then c
+          else if k-depth <= lv then lift_substituend depth lamv.(k-depth-1)
+          else mkRel (k-lv)
+      | _ -> map_constr_with_binders succ substrec depth c in 
+    substrec n c
 
 (*
 let substkey = Profile.declare_profile "substn_many";;
-- 
cgit v1.2.3