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 520db6aca994a6710ba955362387803e8564d7a7..f0a3fa0eb7386ba9747243c4050d718ed2ffeea7 100644 (file)
--- 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