X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=8bdb409e923ed19387be8a66fb1b765492ceb582;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=c8016c0bae5b15df6441de6a1358572caf1eb295;hpb=2bb6c98121db82a1c67565bb528787f2def7192d;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index c8016c0ba..8bdb409e9 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -68,13 +68,13 @@ let refine_term metasenv context uri term ugraph =
 	CicRefine.type_of_aux' metasenv context term ugraph in
 	(Ok (term', metasenv')),ugraph1
     with
-      | CicRefine.Uncertain s ->
-          debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force s) ^ "] " ^ CicPp.ppterm term)) ;
-          Uncertain s,ugraph
+      | CicRefine.Uncertain msg ->
+          debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
+          Uncertain (msg (*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 msg,ugraph
+          Ko (msg (*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 = []);
@@ -83,13 +83,13 @@ let refine_obj metasenv context uri obj ugraph =
      let obj', metasenv,ugraph = CicRefine.typecheck metasenv uri obj in
        (Ok (obj', metasenv)),ugraph
    with
-     | CicRefine.Uncertain s ->
-         debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force s) ^ "] " ^ CicPp.ppobj obj)) ;
-         Uncertain s,ugraph
+     | CicRefine.Uncertain msg ->
+         debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ;
+         Uncertain (msg (*lazy ("Uncertain trying to refine: " ^ CicPp.ppobj obj ^ "\n" ^ Lazy.force msg)*)),ugraph
      | CicRefine.RefineFailure msg ->
          debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
            (CicPp.ppobj obj) (Lazy.force msg))) ;
-         Ko msg,ugraph
+         Ko (msg (*lazy ("Error trying to refine: " ^ CicPp.ppobj obj ^ "\n" ^ Lazy.force msg)*)),ugraph
 
 let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
   try
@@ -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 =
@@ -803,7 +818,7 @@ in refine_profiler.HExtlib.profile foo ()
         | Invalid_choice msg -> Ko msg, ugraph
       in
       (* (4) build all possible interpretations *)
-      let (@@) (l1,l2) (l1',l2') = l1@l1, l2@l2' in
+      let (@@) (l1,l2) (l1',l2') = l1@l1', l2@l2' in
       let rec aux aliases diff lookup_in_todo_dom todo_dom base_univ =
         match todo_dom with
         | [] ->