From f2ee9a17174dc0ec833d4caef7d16cdcf8c08302 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 4 Dec 2001 09:50:17 +0000
Subject: [PATCH] lift 0 was just a very heavy implementation of the identity
 function.

---
 helm/ocaml/cic_proof_checking/cicSubstitution.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

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 =
-- 
2.39.2