5 files changed, 112 insertions, 193 deletions

diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml
index ac89dfd747..274dbfd7ed 100644
--- a/pretyping/coercionops.ml
+++ b/pretyping/coercionops.ml
@@ -34,6 +34,31 @@ type cl_info_typ = {
   cl_param : int
 }
 
+let cl_typ_ord t1 t2 = match t1, t2 with
+  | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2
+  | CL_CONST c1, CL_CONST c2 -> Constant.CanOrd.compare c1 c2
+  | CL_PROJ c1, CL_PROJ c2 -> Projection.Repr.CanOrd.compare c1 c2
+  | CL_IND i1, CL_IND i2 -> Ind.CanOrd.compare i1 i2
+  | _ -> pervasives_compare t1 t2 (** OK *)
+
+let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0
+
+module ClTyp = struct
+  type t = cl_typ
+  let compare = cl_typ_ord
+end
+
+module ClPairOrd =
+struct
+  type t = cl_typ * cl_typ
+  let compare (i1, j1) (i2, j2) =
+    let c = cl_typ_ord i1 i2 in
+    if Int.equal c 0 then cl_typ_ord j1 j2 else c
+end
+
+module ClTypMap = Map.Make(ClTyp)
+module ClPairMap = Map.Make(ClPairOrd)
+
 type coe_typ = GlobRef.t
 
 module CoeTypMap = GlobRef.Map_env
@@ -43,6 +68,8 @@ type coe_info_typ = {
   coe_local : bool;
   coe_is_identity : bool;
   coe_is_projection : Projection.Repr.t option;
+  coe_source : cl_typ;
+  coe_target : cl_typ;
   coe_param : int;
 }
 
@@ -53,88 +80,26 @@ let coe_info_typ_equal c1 c2 =
     c1.coe_is_projection == c2.coe_is_projection &&
     Int.equal c1.coe_param c2.coe_param
 
-let cl_typ_ord t1 t2 = match t1, t2 with
-  | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2
-  | CL_CONST c1, CL_CONST c2 -> Constant.CanOrd.compare c1 c2
-  | CL_PROJ c1, CL_PROJ c2 -> Projection.Repr.CanOrd.compare c1 c2
-  | CL_IND i1, CL_IND i2 -> Ind.CanOrd.compare i1 i2
-  | _ -> pervasives_compare t1 t2 (** OK *)
-
-module ClTyp = struct
-  type t = cl_typ
-  let compare = cl_typ_ord
-end
-
-module ClTypMap = Map.Make(ClTyp)
-
-let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0
-
 type inheritance_path = coe_info_typ list
 
-(* table des classes, des coercions et graphe d'heritage *)
-
-module Bijint :
-sig
-  module Index :
-  sig
-    type t
-    val compare : t -> t -> int
-    val equal : t -> t -> bool
-    val print : t -> Pp.t
-  end
-  type 'a t
-  val empty : 'a t
-  val mem : cl_typ -> 'a t -> bool
-  val map : Index.t -> 'a t -> cl_typ * 'a
-  val revmap : cl_typ -> 'a t -> Index.t * 'a
-  val add : cl_typ -> 'a -> 'a t -> 'a t
-  val dom : 'a t -> cl_typ list
-end
-=
-struct
-
-  module Index = struct include Int let print = Pp.int end
-
-  type 'a t = { v : (cl_typ * 'a) Int.Map.t; s : int; inv : int ClTypMap.t }
-  let empty = { v = Int.Map.empty; s = 0; inv = ClTypMap.empty }
-  let mem y b = ClTypMap.mem y b.inv
-  let map x b = Int.Map.find x b.v
-  let revmap y b = let n = ClTypMap.find y b.inv in (n, snd (Int.Map.find n b.v))
-  let add x y b =
-    { v = Int.Map.add b.s (x,y) b.v; s = b.s+1; inv = ClTypMap.add x b.s b.inv }
-  let dom b = List.rev (ClTypMap.fold (fun x _ acc -> x::acc) b.inv [])
-end
-
-type cl_index = Bijint.Index.t
-
 let init_class_tab =
-  let open Bijint in
+  let open ClTypMap in
   add CL_FUN { cl_param = 0 } (add CL_SORT { cl_param = 0 } empty)
 
 let class_tab =
-  Summary.ref ~name:"class_tab" (init_class_tab : cl_info_typ Bijint.t)
+  Summary.ref ~name:"class_tab" (init_class_tab : cl_info_typ ClTypMap.t)
 
 let coercion_tab =
   Summary.ref ~name:"coercion_tab" (CoeTypMap.empty : coe_info_typ CoeTypMap.t)
 
-module ClPairOrd =
-struct
-  type t = cl_index * cl_index
-  let compare (i1, j1) (i2, j2) =
-    let c = Bijint.Index.compare i1 i2 in
-    if Int.equal c 0 then Bijint.Index.compare j1 j2 else c
-end
-
-module ClPairMap = Map.Make(ClPairOrd)
-
 let inheritance_graph =
   Summary.ref ~name:"inheritance_graph" (ClPairMap.empty : inheritance_path ClPairMap.t)
 
 (* ajout de nouveaux "objets" *)
 
 let add_new_class cl s =
-  if not (Bijint.mem cl !class_tab) then
-    class_tab := Bijint.add cl s !class_tab
+  if not (ClTypMap.mem cl !class_tab) then
+    class_tab := ClTypMap.add cl s !class_tab
 
 let add_new_coercion coe s =
   coercion_tab := CoeTypMap.add coe s !coercion_tab
@@ -144,17 +109,9 @@ let add_new_path x y =
 
 (* class_info : cl_typ -> int * cl_info_typ *)
 
-let class_info cl = Bijint.revmap cl !class_tab
-
-let class_exists cl = Bijint.mem cl !class_tab
-
-(* class_info_from_index : int -> cl_typ * cl_info_typ *)
+let class_info cl = ClTypMap.find cl !class_tab
 
-let class_info_from_index i = Bijint.map i !class_tab
-
-let cl_fun_index = fst(class_info CL_FUN)
-
-let cl_sort_index = fst(class_info CL_SORT)
+let class_exists cl = ClTypMap.mem cl !class_tab
 
 let coercion_info coe = CoeTypMap.find coe !coercion_tab
 
@@ -200,20 +157,18 @@ let subst_coe_typ subst t = subst_global_reference subst t
 (* class_of : Term.constr -> int *)
 
 let class_of env sigma t =
-  let (t, n1, i, u, args) =
+  let (t, n1, cl, u, args) =
     try
       let (cl, u, args) = find_class_type env sigma t in
-      let (i, { cl_param = n1 } ) = class_info cl in
-      (t, n1, i, u, args)
+      let { cl_param = n1 } = class_info cl in
+      (t, n1, cl, u, args)
     with Not_found ->
       let t = Tacred.hnf_constr env sigma t in
       let (cl, u, args) = find_class_type env sigma t in
-      let (i, { cl_param = n1 } ) = class_info cl in
-      (t, n1, i, u, args)
+      let { cl_param = n1 } = class_info cl in
+      (t, n1, cl, u, args)
   in
-  if Int.equal (List.length args) n1 then t, i else raise Not_found
-
-let inductive_class_of ind = fst (class_info (CL_IND ind))
+  if Int.equal (List.length args) n1 then t, cl else raise Not_found
 
 let class_args_of env sigma c = pi3 (find_class_type env sigma c)
 
@@ -238,26 +193,26 @@ let lookup_path_between_class (s,t) =
   ClPairMap.find (s,t) !inheritance_graph
 
 let lookup_path_to_fun_from_class s =
-  lookup_path_between_class (s,cl_fun_index)
+  lookup_path_between_class (s, CL_FUN)
 
 let lookup_path_to_sort_from_class s =
-  lookup_path_between_class (s,cl_sort_index)
+  lookup_path_between_class (s, CL_SORT)
 
 (* advanced path lookup *)
 
 let apply_on_class_of env sigma t cont =
   try
     let (cl,u,args) = find_class_type env sigma t in
-    let (i, { cl_param = n1 } ) = class_info cl in
+    let { cl_param = n1 } = class_info cl in
     if not (Int.equal (List.length args) n1) then raise Not_found;
-    t, cont i
+    t, cont cl
   with Not_found ->
     (* Is it worth to be more incremental on the delta steps? *)
     let t = Tacred.hnf_constr env sigma t in
     let (cl, u, args) = find_class_type env sigma t in
-    let (i, { cl_param = n1 } ) = class_info cl in
+    let { cl_param = n1 } = class_info cl in
     if not (Int.equal (List.length args) n1) then raise Not_found;
-    t, cont i
+    t, cont cl
 
 let lookup_path_between env sigma (s,t) =
   let (s,(t,p)) =
@@ -287,25 +242,25 @@ let get_coercion_constructor env coe =
   | _ -> raise Not_found
 
 let lookup_pattern_path_between env (s,t) =
-  let i = inductive_class_of s in
-  let j = inductive_class_of t in
-  List.map (get_coercion_constructor env) (ClPairMap.find (i,j) !inheritance_graph)
+  List.map (get_coercion_constructor env)
+    (ClPairMap.find (CL_IND s, CL_IND t) !inheritance_graph)
 
 (* rajouter une coercion dans le graphe *)
 
-let path_printer : ((cl_index * cl_index) * inheritance_path -> Pp.t) ref =
+let path_printer : ((cl_typ * cl_typ) * inheritance_path -> Pp.t) ref =
   ref (fun _ -> str "<a class path>")
 
 let install_path_printer f = path_printer := f
 
 let print_path x = !path_printer x
 
-let path_comparator : (Environ.env -> Evd.evar_map -> cl_index -> inheritance_path -> inheritance_path -> bool) ref =
+let path_comparator :
+  (Environ.env -> Evd.evar_map -> cl_typ -> inheritance_path -> inheritance_path -> bool) ref =
   ref (fun _ _ _ _ _ -> false)
 
 let install_path_comparator f = path_comparator := f
 
-let compare_path p q = !path_comparator p q
+let compare_path env sigma cl p q = !path_comparator env sigma cl p q
 
 let warn_ambiguous_path =
   CWarnings.create ~name:"ambiguous-paths" ~category:"typechecker"
@@ -316,29 +271,29 @@ let warn_ambiguous_path =
          else
            str" is ambiguous with existing " ++ print_path (c, q) ++ str".") l)
 
-(* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit
+(* add_coercion_in_graph : coe_index * cl_typ * cl_typ -> unit
                          coercion,source,target *)
 
-let different_class_params env i =
-  let ci = class_info_from_index i in
-    if (snd ci).cl_param > 0 then true
-    else
-      match fst ci with
-      | CL_IND i -> Environ.is_polymorphic env (GlobRef.IndRef i)
-      | CL_CONST c -> Environ.is_polymorphic env (GlobRef.ConstRef c)
-      | _ -> false
+let different_class_params env ci =
+  if (class_info ci).cl_param > 0 then true
+  else
+    match ci with
+    | CL_IND i -> Environ.is_polymorphic env (GlobRef.IndRef i)
+    | CL_CONST c -> Environ.is_polymorphic env (GlobRef.ConstRef c)
+    | _ -> false
 
-let add_coercion_in_graph env sigma (ic,source,target) =
+let add_coercion_in_graph env sigma ic =
   let old_inheritance_graph = !inheritance_graph in
-  let ambig_paths =
-    (ref [] : ((cl_index * cl_index) * inheritance_path * inheritance_path) list ref) in
+  let ambig_paths :
+    ((cl_typ * cl_typ) * inheritance_path * inheritance_path) list ref =
+    ref [] in
   let try_add_new_path (i,j as ij) p =
     (* If p is a cycle, we check whether p is definitionally an identity
        function or not. If it is not, we report p as an ambiguous inheritance
        path. *)
-    if Bijint.Index.equal i j && not (compare_path env sigma i p []) then
+    if cl_typ_eq i j && not (compare_path env sigma i p []) then
       ambig_paths := (ij,p,[])::!ambig_paths;
-    if not (Bijint.Index.equal i j) || different_class_params env i then
+    if not (cl_typ_eq i j) || different_class_params env i then
       match lookup_path_between_class ij with
       | q ->
         (* p has the same source and target classes as an existing path q. We
@@ -359,45 +314,36 @@ let add_coercion_in_graph env sigma (ic,source,target) =
   let try_add_new_path1 ij p =
     let _ = try_add_new_path ij p in ()
   in
-  if try_add_new_path (source,target) [ic] then begin
+  if try_add_new_path (ic.coe_source, ic.coe_target) [ic] then begin
     ClPairMap.iter
       (fun (s,t) p ->
-         if not (Bijint.Index.equal s t) then begin
-           if Bijint.Index.equal t source then begin
-             try_add_new_path1 (s,target) (p@[ic]);
+         if not (cl_typ_eq s t) then begin
+           if cl_typ_eq t ic.coe_source then begin
+             try_add_new_path1 (s, ic.coe_target) (p@[ic]);
              ClPairMap.iter
                (fun (u,v) q ->
-                  if not (Bijint.Index.equal u v) && Bijint.Index.equal u target then
+                  if not (cl_typ_eq u v) && cl_typ_eq u ic.coe_target then
                     try_add_new_path1 (s,v) (p@[ic]@q))
                old_inheritance_graph
            end;
-           if Bijint.Index.equal s target then try_add_new_path1 (source,t) (ic::p)
+           if cl_typ_eq s ic.coe_target then
+             try_add_new_path1 (ic.coe_source, t) (ic::p)
          end)
       old_inheritance_graph
   end;
   match !ambig_paths with [] -> () | _ -> warn_ambiguous_path !ambig_paths
 
-type coercion = {
-  coercion_type   : coe_typ;
-  coercion_local  : bool;
-  coercion_is_id  : bool;
-  coercion_is_proj  : Projection.Repr.t option;
-  coercion_source : cl_typ;
-  coercion_target : cl_typ;
-  coercion_params : int;
-}
-
 let subst_coercion subst c =
   let env = Global.env () in
-  let coe = subst_coe_typ subst c.coercion_type in
-  let cls = subst_cl_typ env subst c.coercion_source in
-  let clt = subst_cl_typ env subst c.coercion_target in
-  let clp = Option.Smart.map (subst_proj_repr subst) c.coercion_is_proj in
-  if c.coercion_type == coe && c.coercion_source == cls &&
-     c.coercion_target == clt && c.coercion_is_proj == clp
+  let coe = subst_coe_typ subst c.coe_value in
+  let cls = subst_cl_typ env subst c.coe_source in
+  let clt = subst_cl_typ env subst c.coe_target in
+  let clp = Option.Smart.map (subst_proj_repr subst) c.coe_is_projection in
+  if c.coe_value == coe && c.coe_source == cls && c.coe_target == clt &&
+     c.coe_is_projection == clp
   then c
-  else { c with coercion_type = coe; coercion_source = cls;
-                coercion_target = clt; coercion_is_proj = clp; }
+  else { c with coe_value = coe; coe_source = cls; coe_target = clt;
+                coe_is_projection = clp; }
 
 (* Computation of the class arity *)
 
@@ -422,24 +368,14 @@ let add_class env sigma cl =
   add_new_class cl { cl_param = class_params env sigma cl }
 
 let declare_coercion env sigma c =
-  let () = add_class env sigma c.coercion_source in
-  let () = add_class env sigma c.coercion_target in
-  let is, _ = class_info c.coercion_source in
-  let it, _ = class_info c.coercion_target in
-  let xf =
-    { coe_value = c.coercion_type;
-      coe_local = c.coercion_local;
-      coe_is_identity = c.coercion_is_id;
-      coe_is_projection = c.coercion_is_proj;
-      coe_param = c.coercion_params;
-    } in
-  let () = add_new_coercion c.coercion_type xf in
-  add_coercion_in_graph env sigma (xf,is,it)
+  let () = add_class env sigma c.coe_source in
+  let () = add_class env sigma c.coe_target in
+  let () = add_new_coercion c.coe_value c in
+  add_coercion_in_graph env sigma c
 
 (* For printing purpose *)
-let pr_cl_index = Bijint.Index.print
-
-let classes () = Bijint.dom !class_tab
+let classes () =
+  List.rev (ClTypMap.fold (fun x _ acc -> x :: acc) !class_tab [])
 let coercions () =
   List.rev (CoeTypMap.fold (fun _ y acc -> y::acc) !coercion_tab [])
 
diff --git a/pretyping/coercionops.mli b/pretyping/coercionops.mli
index 073500b155..fb5621dd3a 100644
--- a/pretyping/coercionops.mli
+++ b/pretyping/coercionops.mli
@@ -44,12 +44,11 @@ type coe_info_typ = {
   coe_local : bool;
   coe_is_identity : bool;
   coe_is_projection : Projection.Repr.t option;
+  coe_source : cl_typ;
+  coe_target : cl_typ;
   coe_param : int;
 }
 
-(** [cl_index] is the type of class keys *)
-type cl_index
-
 (** This is the type of paths from a class to another *)
 type inheritance_path = coe_info_typ list
 
@@ -57,37 +56,21 @@ type inheritance_path = coe_info_typ list
 
 val class_exists : cl_typ -> bool
 
-val class_info : cl_typ -> (cl_index * cl_info_typ)
 (** @raise Not_found if this type is not a class *)
-
-val class_info_from_index : cl_index -> cl_typ * cl_info_typ
+val class_info : cl_typ -> cl_info_typ
 
 (** [find_class_type env sigma c] returns the head reference of [c],
     its universe instance and its arguments *)
 val find_class_type : env -> evar_map -> types -> cl_typ * EInstance.t * constr list
 
 (** raises [Not_found] if not convertible to a class *)
-val class_of : env -> evar_map -> types -> types * cl_index
-
-(** raises [Not_found] if not mapped to a class *)
-val inductive_class_of : inductive -> cl_index
+val class_of : env -> evar_map -> types -> types * cl_typ
 
 val class_args_of : env -> evar_map -> types -> constr list
 
-(** {6 [declare_coercion] adds a coercion in the graph of coercion paths } *)
-type coercion = {
-  coercion_type   : coe_typ;
-  coercion_local  : bool;
-  coercion_is_id  : bool;
-  coercion_is_proj  : Projection.Repr.t option;
-  coercion_source : cl_typ;
-  coercion_target : cl_typ;
-  coercion_params : int;
-}
-
-val subst_coercion : substitution -> coercion -> coercion
+val subst_coercion : substitution -> coe_info_typ -> coe_info_typ
 
-val declare_coercion : env -> evar_map -> coercion -> unit
+val declare_coercion : env -> evar_map -> coe_info_typ -> unit
 
 (** {6 Access to coercions infos } *)
 val coercion_exists : coe_typ -> bool
@@ -98,7 +81,7 @@ val coercion_info : coe_typ -> coe_info_typ
 
 (** @raise Not_found in the following functions when no path exists *)
 
-val lookup_path_between_class : cl_index * cl_index -> inheritance_path
+val lookup_path_between_class : cl_typ * cl_typ -> inheritance_path
 val lookup_path_between : env -> evar_map -> types * types ->
       types * types * inheritance_path
 val lookup_path_to_fun_from : env -> evar_map -> types ->
@@ -111,16 +94,15 @@ val lookup_pattern_path_between :
 (**/**)
 (* Crade *)
 val install_path_printer :
-  ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
+  ((cl_typ * cl_typ) * inheritance_path -> Pp.t) -> unit
 val install_path_comparator :
-  (env -> evar_map -> cl_index -> inheritance_path -> inheritance_path -> bool) -> unit
+  (env -> evar_map -> cl_typ -> inheritance_path -> inheritance_path -> bool) -> unit
 (**/**)
 
 (** {6 This is for printing purpose } *)
 val string_of_class : cl_typ -> string
 val pr_class : cl_typ -> Pp.t
-val pr_cl_index : cl_index -> Pp.t
-val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list
+val inheritance_graph : unit -> ((cl_typ * cl_typ) * inheritance_path) list
 val classes : unit -> cl_typ list
 val coercions : unit -> coe_info_typ list
 
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 2c107502f4..b19dbd46be 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -135,8 +135,9 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs =
 
 
 let construct_of_constr const env sigma tag typ =
-  let t, l = app_type env typ in
-  match EConstr.kind_upto sigma t with
+  let typ = Reductionops.clos_whd_flags CClosure.all env sigma (EConstr.of_constr typ) in
+  let t, l = decompose_appvect (EConstr.Unsafe.to_constr typ) in
+  match Constr.kind t with
   | Ind (ind,u) ->
       construct_of_constr_notnative const env tag ind u l
   | _ ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e86a8a28c9..3ccc6ea125 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1398,7 +1398,7 @@ let understand_ltac flags env sigma lvar kind c =
   let (sigma, c, _) = ise_pretype_gen flags env sigma lvar kind c in
   (sigma, c)
 
-let path_convertible env sigma i p q =
+let path_convertible env sigma cl p q =
   let open Coercionops in
   let mkGRef ref          = DAst.make @@ Glob_term.GRef(ref,None) in
   let mkGVar id           = DAst.make @@ Glob_term.GVar(id) in
@@ -1423,7 +1423,7 @@ let path_convertible env sigma i p q =
           p'
     | [] ->
       (* identity function for the class [i]. *)
-      let cl,params = class_info_from_index i in
+      let params = (class_info cl).cl_param in
       let clty =
         match cl with
         | CL_SORT -> mkGSort (Glob_term.UAnonymous {rigid=false})
@@ -1434,8 +1434,7 @@ let path_convertible env sigma i p q =
         | CL_PROJ p -> mkGRef (GlobRef.ConstRef (Projection.Repr.constant p))
       in
       let names =
-        List.init params.cl_param
-          (fun n -> Id.of_string ("x" ^ string_of_int n))
+        List.init params (fun n -> Id.of_string ("x" ^ string_of_int n))
       in
       List.fold_right
         (fun id t -> mkGLambda (Name id, mkGHole (), t)) names @@
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index cf6d581066..9939764069 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -78,8 +78,9 @@ let type_constructor mind mib u (ctx, typ) params =
 
 
 
-let construct_of_constr const env tag typ =
-  let (t, allargs) = decompose_appvect (whd_all env typ) in
+let construct_of_constr const env sigma tag typ =
+  let typ = Reductionops.clos_whd_flags CClosure.all env sigma (EConstr.of_constr typ) in
+  let t, allargs = decompose_appvect (EConstr.Unsafe.to_constr typ) in
   match Constr.kind t with
   | Ind ((mind,_ as ind), u as indu) ->
     let mib,mip = lookup_mind_specif env ind in
@@ -92,8 +93,8 @@ let construct_of_constr const env tag typ =
      assert (Constr.equal t (Typeops.type_of_int env));
       (mkInt (Uint63.of_int tag), t)
 
-let construct_of_constr_const env tag typ =
-  fst (construct_of_constr true env tag typ)
+let construct_of_constr_const env sigma tag typ =
+  fst (construct_of_constr true env sigma tag typ)
 
 let construct_of_constr_block = construct_of_constr false
 
@@ -156,7 +157,7 @@ and nf_whd env sigma whd typ =
       let _, args = nf_args env sigma vargs t in
       mkApp(cfd,args)
   | Vconstr_const n ->
-    construct_of_constr_const env n typ
+    construct_of_constr_const env sigma n typ
   | Vconstr_block b ->
       let tag = btag b in
       let (tag,ofs) =
@@ -165,7 +166,7 @@ and nf_whd env sigma whd typ =
           | Vconstr_const tag -> (tag+Obj.last_non_constant_constructor_tag, 1)
           | _ -> assert false
         else (tag, 0) in
-      let capp,ctyp = construct_of_constr_block env tag typ in
+      let capp,ctyp = construct_of_constr_block env sigma tag typ in
       let args = nf_bargs env sigma b ofs ctyp in
       mkApp(capp,args)
   | Vint64 i -> i |> Uint63.of_int64 |> mkInt
@@ -414,9 +415,9 @@ let cbv_vm env sigma c t  =
   if Termops.occur_meta sigma c then
     CErrors.user_err Pp.(str "vm_compute does not support metas.");
   (* This evar-normalizes terms beforehand *)
-  let c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
-  let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in
-  let v = Vmsymtable.val_of_constr env c in
+  let c = EConstr.Unsafe.to_constr c in
+  let t = EConstr.Unsafe.to_constr t in
+  let v = Vmsymtable.val_of_constr env (Evd.existential_opt_value0 sigma) c in
   EConstr.of_constr (nf_val env sigma v t)
 
 let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 =