Merge PR #935: Handling evars in the VM

1 files changed, 8 insertions, 3 deletions

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 586ef1709..6ed1ba539 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -180,6 +180,7 @@ type fv_elem =
   | FVnamed of Id.t
   | FVrel of int
   | FVuniv_var of int
+  | FVevar of Evar.t
 
 type fv = fv_elem array
 
@@ -194,12 +195,15 @@ type t = fv_elem
 
 let compare e1 e2 = match e1, e2 with
 | FVnamed id1, FVnamed id2 -> Id.compare id1 id2
-| FVnamed _, _ -> -1
+| FVnamed _, (FVrel _ | FVuniv_var _ | FVevar _) -> -1
 | FVrel _, FVnamed _ -> 1
 | FVrel r1, FVrel r2 -> Int.compare r1 r2
-| FVrel _, FVuniv_var _ -> -1
+| FVrel _, (FVuniv_var _ | FVevar _) -> -1
 | FVuniv_var i1, FVuniv_var i2 -> Int.compare i1 i2
-| FVuniv_var i1, _ -> 1
+| FVuniv_var i1, (FVnamed _ | FVrel _) -> 1
+| FVuniv_var i1, FVevar _ -> -1
+| FVevar _, (FVnamed _ | FVrel _ | FVuniv_var _) -> 1
+| FVevar e1, FVevar e2 -> Evar.compare e1 e2
 
 end
 
@@ -252,6 +256,7 @@ let pp_fv_elem = function
   | FVnamed id -> str "FVnamed(" ++ Id.print id ++ str ")"
   | FVrel i -> str "Rel(" ++ int i ++ str ")"
   | FVuniv_var v -> str "FVuniv(" ++ int v ++ str ")"
+  | FVevar e -> str "FVevar(" ++ int (Evar.repr e) ++ str ")"
 
 let rec pp_instr i =
   match i with