From f3a40daf813df6d33289d4df64da6c16ea9d3ca4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 8 May 2009 15:00:03 +0000 Subject: [PATCH] Bug fixed in interpretation of records (the type was unbound in the fields). --- .../components/ng_disambiguation/nCicDisambiguate.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 520db6aca..f0a3fa0eb 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -570,19 +570,20 @@ let interpretate_obj add_params (interpretate_term ~obj_context:[] ~context ~env ~uri:None ~is_path:false ty) in + let nref = + NReference.reference_of_spec uri (NReference.Ind (true,0,leftno)) in + let obj_context = [name,nref] in let fields' = snd ( List.fold_left (fun (context,res) (name,ty,_coercion,_arity) -> let ty = - interpretate_term ~obj_context:[] ~context ~env ~uri:None + interpretate_term ~obj_context ~context ~env ~uri:None ~is_path:false ty in let context' = (name,NCic.Decl ty)::context in context',(name,ty)::res ) (context,[]) fields) in let concl = - let nref = - NReference.reference_of_spec uri (NReference.Ind (true,0,leftno)) in let mutind = NCic.Const nref in if params = [] then mutind else -- 2.39.2