Bug: types and terms pushed into the context must be Implicit free.

Partial fix committed (types of Fix and CoFix not patched yet).

diff --git a/helm/software/components/cic/deannotate.ml b/helm/software/components/cic/deannotate.ml
index 69eccd9b9897dec7044791e0979a1c07bbe74760..ace1e60007b54e9013d57483dffd237e85526327 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 so = compute_letin_type context so in
        let ty = !type_of_aux' context so in
-        C.LetIn (name,
-         compute_letin_type context so,
-         ty,
+        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)