From 68f93b859c6b978bfd66c03fb383985f835f6657 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 19 Mar 2008 19:25:25 +0000 Subject: [PATCH] Bug: types and terms pushed into the context must be Implicit free. Partial fix committed (types of Fix and CoFix not patched yet). --- helm/software/components/cic/deannotate.ml | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) 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) -- 2.39.2