End of patch for computation of LetIn types. Now types of mutually (co)recursive

function are added to the environment _after_ Implicit have been resolved.

diff --git a/helm/software/components/cic/deannotate.ml b/helm/software/components/cic/deannotate.ml
index ace1e60007b54e9013d57483dffd237e85526327..e81190842c6ff2e09c53e1c7bcc9ac9cb7c87bf8 100644 (file)
--- a/helm/software/components/cic/deannotate.ml
+++ b/helm/software/components/cic/deannotate.ml
@@ -164,6 +164,10 @@ let rec compute_letin_type context te =
         compute_letin_type context te,
         List.map (fun x -> compute_letin_type context x) pl)
     | C.Fix (fno,fl) ->
+        let fl =
+         List.map
+          (function (name,recno,ty,bo) ->
+            name,recno,compute_letin_type context ty, bo) fl in
         let tys,_ =
          List.fold_left
           (fun (types,len) (n,_,ty,_) ->
@@ -174,11 +178,13 @@ let rec compute_letin_type context te =
          C.Fix (fno,
           List.map
            (fun (name,recno,ty,bo) ->
-             name, recno,
-             compute_letin_type context ty,
-             compute_letin_type (tys @ context) bo
+             name, recno, ty, compute_letin_type (tys @ context) bo
            ) fl)
     | C.CoFix (fno,fl) ->
+        let fl =
+         List.map
+          (function (name,ty,bo) ->
+            name, compute_letin_type context ty, bo) fl in
         let tys,_ =
          List.fold_left
           (fun (types,len) (n,ty,_) ->
@@ -189,9 +195,7 @@ let rec compute_letin_type context te =
          C.CoFix (fno,
           List.map
            (fun (name,ty,bo) ->
-             name,
-             compute_letin_type context ty,
-             compute_letin_type (tys @ context) bo
+             name, ty, compute_letin_type (tys @ context) bo
            ) fl)
 ;;