Bug fixed: the ens need not be ordered w.r.t. the declared variables.

The latter order is the right one for abstraction.

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 54e12be14ae6fe3bcdda32c5fa6e393770ee09b2..3493dbff59077b0d7af1375dcf5333234c517324 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -263,7 +263,7 @@ let convert_term uri t =
         | (NCic.Appl l1)::l2 -> NCic.Appl (l1@l2), fixpoints
         | _ -> NCic.Appl l, fixpoints)
     | Cic.Const (curi, ens) -> 
-       aux_ens octx ctx n_fix uri ens
+       aux_ens curi octx ctx n_fix uri ens
         (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
         | Cic.Constant (_,Some _,_,_,_) ->
                NCic.Const (Ref.reference_of_ouri curi Ref.Def)
@@ -271,10 +271,10 @@ let convert_term uri t =
                NCic.Const (Ref.reference_of_ouri curi Ref.Decl)
         | _ -> assert false)
     | Cic.MutInd (curi, tyno, ens) -> 
-       aux_ens octx ctx n_fix uri ens
+       aux_ens curi octx ctx n_fix uri ens
         (NCic.Const (Ref.reference_of_ouri curi (Ref.Ind tyno)))
     | Cic.MutConstruct (curi, tyno, consno, ens) -> 
-       aux_ens octx ctx n_fix uri ens
+       aux_ens curi octx ctx n_fix uri ens
         (NCic.Const (Ref.reference_of_ouri curi (Ref.Con (tyno,consno))))
     | Cic.MutCase (curi, tyno, outty, t, branches) ->
         let outty = fix_outty curi tyno t octx outty in
@@ -290,16 +290,24 @@ let convert_term uri t =
         in
         NCic.Match (r,outty,t,branches), fixpoints_outty@fixpoints_t@fixpoints
     | Cic.Implicit _ | Cic.Meta _ | Cic.Var _ -> assert false
-  and aux_ens octx ctx n_fix uri ens he =
+  and aux_ens curi octx ctx n_fix uri ens he =
    match ens with
       [] -> he,[]
     | _::_ ->
+      let params =
+       match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
+          Cic.Constant (_,_,_,params,_)
+        | Cic.InductiveDefinition (_,params,_,_) -> params
+        | Cic.Variable _
+        | Cic.CurrentProof _ -> assert false
+      in
       let ens,objs =
        List.fold_right
-        (fun (_,t) (l,objs) ->
+        (fun uri (l,objs) ->
+          let t = List.assoc uri ens in
           let t,o = aux octx ctx n_fix uri t in
            t::l, o@objs
-        ) ens ([],[])
+        ) params ([],[])
       in
        NCic.Appl (he::ens),objs
   in
@@ -308,22 +316,19 @@ let convert_term uri t =
 
 let cook mode vars t =
  let t = CicSubstitution.lift (List.length vars) t in
- snd (List.fold_right
-  (fun uri (n,t) ->
+ List.fold_right
+  (fun uri t ->
     let t = CicSubstitution.subst_vars [uri,Cic.Rel 1] t in
     let bo,ty =
      match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
         Cic.Variable (_,bo,ty,_,_) -> bo,ty
       | _ -> assert false in
     let id = Cic.Name (UriManager.name_of_uri uri) in
-    let t =
      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)
-    in
-     n+1,t
-  ) vars (1,t))
+  ) vars t
 ;;
 
 let convert_obj_aux uri = function