"let rec f = ... in f l" used to be compiled incorrectly

[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index de3701e23401e8cec86445ce5ecbbb4a041a9337..f8fa77dc67b894f6bc5a77f2a820ac65942f2f75 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -70,11 +70,11 @@ let refine_term metasenv context uri term ugraph =
     with
       | CicRefine.Uncertain msg ->
           debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
-          Uncertain (lazy ("Uncertain trying to refine: " ^ CicPp.ppterm term ^ "\n" ^ Lazy.force msg)),ugraph
+          Uncertain (lazy ("Uncertain trying to refine: " ^ CicMetaSubst.ppterm_in_context [] term context ^ "\n" ^ Lazy.force msg)),ugraph
       | CicRefine.RefineFailure msg ->
           debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
             (CicPp.ppterm term) (Lazy.force msg)));
-          Ko (lazy ("Error trying to refine: " ^ CicPp.ppterm term ^ "\n" ^ Lazy.force msg)),ugraph
+          Ko (lazy ("Error trying to refine: " ^ CicMetaSubst.ppterm_in_context [] term context ^ "\n" ^ Lazy.force msg)),ugraph
 
 let refine_obj metasenv context uri obj ugraph =
  assert (context = []);
@@ -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 =