added profiling on/off

[helm.git] / helm / software / components / ng_kernel / oCic2NCic.ml

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index cc675d2768eca313934f6db3082322c31ad37331..5b4d9f9e1222378768044194fd159b99f2902547 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -357,6 +357,11 @@ let convert_term uri t =
     | Cic.MutConstruct (curi, tyno, consno, ens) -> 
        aux_ens curi octx ctx n_fix uri ens
         (NCic.Const (Ref.reference_of_ouri curi (Ref.Con (tyno,consno))))
+    | Cic.Var (curi, ens) ->
+       (match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
+           Cic.Variable (_,Some bo,_,_,_) ->
+            aux octx ctx n_fix uri (CicSubstitution.subst_vars ens bo)
+         | _ -> assert false)
     | Cic.MutCase (curi, tyno, outty, t, branches) ->
         let r = Ref.reference_of_ouri curi (Ref.Ind tyno) in
         let outty, fixpoints_outty = aux octx ctx n_fix uri outty in
@@ -369,7 +374,7 @@ let convert_term uri t =
              branches ([],[])
         in
         NCic.Match (r,outty,t,branches), fixpoints_outty@fixpoints_t@fixpoints
-    | Cic.Implicit _ | Cic.Meta _ | Cic.Var _ -> assert false
+    | Cic.Implicit _ | Cic.Meta _ -> assert false
   and aux_ens curi octx ctx n_fix uri ens he =
    match ens with
       [] -> he,[]
@@ -385,11 +390,9 @@ let convert_term uri t =
        List.fold_right
         (fun luri (l,objs) ->
           match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph luri) with
-             Cic.Variable (_,bo,_,_,_) ->
-              let t =
-               match bo with
-                  None -> List.assoc luri ens
-                | Some t -> CicSubstitution.subst_vars ens t in
+             Cic.Variable (_,Some _,_,_,_) -> l, objs
+           | Cic.Variable (_,None,_,_,_) ->
+              let t = List.assoc luri ens in
               let t,o = aux octx ctx n_fix uri t in
                t::l, o@objs
            | _ -> assert false