From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 8 Apr 2008 15:56:31 +0000 (+0000)
Subject: The old kernel does not accept ens whose order is different from the one
X-Git-Tag: make_still_working~5404
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a2642c03bef7812ca81b25da0d3cb2f504e0a0b0;p=helm.git

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 3493dbff5..f54f184d8 100644
--- 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