From f5b76bf5f55bbd2f2053e36d4b251548f3ed8623 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 19 Nov 2005 18:28:15 +0000
Subject: [PATCH] "let rec f = ... in f l" used to be compiled incorrectly
 (without checking if f occurs in l and without delifting l!!!)

---
 helm/ocaml/cic_disambiguation/disambiguate.ml | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index d3f5b0106..f8fa77dc6 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -222,7 +222,22 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast =
                 let fix = Cic.Fix (!counter,funs) in
                  match cic with
                     Cic.Rel 1 -> fix
-                  | (Cic.Appl (Cic.Rel 1::l)) -> Cic.Appl (fix::l)
+                  | (Cic.Appl (Cic.Rel 1::l)) ->
+                     (try
+                       let l' =
+                        List.map
+                         (function t ->
+                           let t',subst,metasenv =
+                            CicMetaSubst.delift_rels [] [] 1 t
+                           in
+                            assert (subst=[]);
+                            assert (metasenv=[]);
+                            t') l
+                       in
+                        Cic.Appl (fix::l')
+                      with
+                       CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
+                        Cic.LetIn (Cic.Name var, fix, cic))
                   | _ -> Cic.LetIn (Cic.Name var, fix, cic))
           | `CoInductive ->
               let funs =
-- 
2.39.2