Avoid generation of let x = let rec x = ... in x in (x ...).

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index f203e6d790edc4b2cc6e413afa8e1c40c6935964..a245053c6cd96fedf4c277a6c6897b5b4710f359 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -109,6 +109,7 @@ let find_in_context name (context: Cic.name list) =
 
 let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast =
   assert (uri = None);
+prerr_endline "ciao";
   let rec aux loc (context: Cic.name list) = function
     | CicNotationPt.AttributedTerm (`Loc loc, term) ->
         aux loc context term
@@ -213,14 +214,22 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast =
           | `Inductive ->
               (fun (var, _, _, _) cic ->
                 incr counter;
-                Cic.LetIn (Cic.Name var, Cic.Fix (!counter, funs), cic))
+                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.LetIn (Cic.Name var, fix, cic))
           | `CoInductive ->
               let funs =
                 List.map (fun (name, _, typ, body) -> (name, typ, body)) funs
               in
               (fun (var, _, _, _) cic ->
                 incr counter;
-                Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic))
+                let cofix = Cic.CoFix (!counter,funs) in
+                 match cic with
+                    Cic.Rel 1 -> cofix
+                  | (Cic.Appl (Cic.Rel 1::l)) -> Cic.Appl (cofix::l)
+                  | _ -> Cic.LetIn (Cic.Name var, cofix, cic))
         in
         List.fold_right (build_term inductiveFuns) inductiveFuns cic_body
     | CicNotationPt.Ident _