From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 8 May 2009 15:00:03 +0000 (+0000)
Subject: Bug fixed in interpretation of records (the type was unbound in the fields).
X-Git-Tag: make_still_working~4009
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f3a40daf813df6d33289d4df64da6c16ea9d3ca4;p=helm.git

Bug fixed in interpretation of records (the type was unbound in the fields).
---

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