CProp hierarchy fixed:

[helm.git] / helm / software / components / cic / deannotate.ml

diff --git a/helm/software/components/cic/deannotate.ml b/helm/software/components/cic/deannotate.ml
index 69eccd9b9897dec7044791e0979a1c07bbe74760..c560af569e031f54a7e37baec625c950fae7d314 100644 (file)
--- a/helm/software/components/cic/deannotate.ml
+++ b/helm/software/components/cic/deannotate.ml
@@ -127,23 +127,22 @@ let rec compute_letin_type context te =
         (compute_letin_type context te,
          compute_letin_type context ty)
     | C.Prod (name,so,dest) ->
-       C.Prod (name,
-        compute_letin_type context so,
+       let so = compute_letin_type context so in
+       C.Prod (name, so,
         compute_letin_type ((Some (name,(C.Decl so)))::context) dest)
     | C.Lambda (name,so,dest) ->
-       C.Lambda (name,
-        compute_letin_type context so,
+       let so = compute_letin_type context so in
+       C.Lambda (name, so,
         compute_letin_type ((Some (name,(C.Decl so)))::context) dest)
     | C.LetIn (name,so,C.Implicit _,dest) ->
-       let ty = !type_of_aux' context so in
-        C.LetIn (name,
-         compute_letin_type context so,
-         ty,
+       let so = compute_letin_type context so in
+       let ty = Unshare.unshare ~fresh_univs:true (!type_of_aux' context so) in
+        C.LetIn (name, so, ty,
          compute_letin_type ((Some (name,(C.Def (so,ty))))::context) dest)
     | C.LetIn (name,so,ty,dest) ->
-       C.LetIn (name,
-        compute_letin_type context so,
-        compute_letin_type context ty,
+       let so = compute_letin_type context so in
+       let ty = compute_letin_type context ty in
+       C.LetIn (name, so, ty,
         compute_letin_type ((Some (name,(C.Def (so,ty))))::context) dest)
     | C.Appl l ->
        C.Appl (List.map (fun x -> compute_letin_type context x) l)
@@ -165,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,_) ->
@@ -175,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,_) ->
@@ -190,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)
 ;;