X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=f0a3fa0eb7386ba9747243c4050d718ed2ffeea7;hb=f3a40daf813df6d33289d4df64da6c16ea9d3ca4;hp=520db6aca994a6710ba955362387803e8564d7a7;hpb=7ce251730873891f2975bc8c46b122e842d203db;p=helm.git

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