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

[helm.git] / helm / ocaml / cic_proof_checking / cicSubstitution.ml

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index 28dbe24e3f40cb73964d86cbf1896fc67d8929e5..a4ca7b5cda395a3ec2923e7c263d52efc21a7777 100644 (file)
--- 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 =