The old kernel does not accept ens whose order is different from the one

declared for the object whose reference it is applied to. Fixed.

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 3493dbff59077b0d7af1375dcf5333234c517324..f54f184d87a2210995ed91d0af4ef2baf86c9fac 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -315,20 +315,29 @@ let convert_term uri t =
 ;;
 
 let cook mode vars t =
- let t = CicSubstitution.lift (List.length vars) t in
- List.fold_right
-  (fun uri t ->
-    let t = CicSubstitution.subst_vars [uri,Cic.Rel 1] t in
+ let varsno = List.length vars in
+ let t = CicSubstitution.lift varsno t in
+ let rec aux n acc l =
+  let subst =
+   snd(List.fold_left (fun (i,res) uri -> i+1,(uri,Cic.Rel i)::res) (1,[]) acc)
+  in
+  match l with
+     [] -> CicSubstitution.subst_vars subst t
+   | uri::uris ->
     let bo,ty =
      match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
         Cic.Variable (_,bo,ty,_,_) -> bo,ty
       | _ -> assert false in
+    let ty = CicSubstitution.subst_vars subst ty in
+    let bo = HExtlib.map_option (CicSubstitution.subst_vars subst) bo in
     let id = Cic.Name (UriManager.name_of_uri uri) in
+    let t = aux (n-1) (uri::acc) uris in
      match bo,ty,mode with
         None,ty,`Lambda -> Cic.Lambda (id,ty,t)
       | None,ty,`Pi -> Cic.Prod (id,ty,t)
       | Some bo,ty,_ -> Cic.LetIn (id,bo,ty,t)
-  ) vars t
+ in
+  aux varsno [] vars
 ;;
 
 let convert_obj_aux uri = function