From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 4 Dec 2001 09:50:17 +0000 (+0000)
Subject: lift 0 was just a very heavy implementation of the identity function.
X-Git-Tag: mlminidom_0_2_2~29
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f2ee9a17174dc0ec833d4caef7d16cdcf8c08302;p=helm.git

lift 0 was just a very heavy implementation of the identity function.
---

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index 28dbe24e3..a4ca7b5cd 100644
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
@@ -65,7 +65,10 @@ let lift n =
        in
         C.CoFix (i, liftedfl)
  in
-  liftaux 1
+  if n = 0 then
+   (function t -> t)
+  else
+   liftaux 1
 ;;
 
 let subst arg =