From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 19 Mar 2008 19:25:25 +0000 (+0000)
Subject: Bug: types and terms pushed into the context must be Implicit free.
X-Git-Tag: make_still_working~5520
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=68f93b859c6b978bfd66c03fb383985f835f6657;p=helm.git

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 69eccd9b9..ace1e6000 100644
--- 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)