From fdd16113a042170022dce276e53e7a3308c0451c Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sun, 30 Aug 2020 09:05:39 +0200
Subject: Remove unchecked arithmetic operations from VM, as they are not used.

---
 kernel/vmlambda.ml | 12 +++---------
 1 file changed, 3 insertions(+), 9 deletions(-)

(limited to 'kernel/vmlambda.ml')

diff --git a/kernel/vmlambda.ml b/kernel/vmlambda.ml
index 332a331a7a..cd7c9b015f 100644
--- a/kernel/vmlambda.ml
+++ b/kernel/vmlambda.ml
@@ -19,8 +19,7 @@ type lambda =
   | Llet          of Name.t Context.binder_annot * lambda * lambda
   | Lapp          of lambda * lambda array
   | Lconst        of pconstant
-  | Lprim         of pconstant option * CPrimitives.t * lambda array
-        (* No check if None *)
+  | Lprim         of pconstant * CPrimitives.t * lambda array
   | Lcase         of case_info * reloc_table * lambda * lambda * lam_branches
   | Lif           of lambda * lambda * lambda
   | Lfix          of (int array * int) * fix_decl
@@ -148,16 +147,11 @@ let rec pp_lam lam =
   | Lval _ -> str "values"
   | Lsort s -> pp_sort s
   | Lind ((mind,i), _) -> MutInd.print mind ++ str"#" ++ int i
-  | Lprim(Some (kn,_u),_op,args) ->
+  | Lprim ((kn,_u),_op,args) ->
      hov 1
          (str "(PRIM " ++ pr_con kn ++  spc() ++
             prlist_with_sep spc pp_lam  (Array.to_list args) ++
             str")")
-  | Lprim(None,op,args) ->
-     hov 1
-         (str "(PRIM_NC " ++ str (CPrimitives.to_string op) ++  spc() ++
-            prlist_with_sep spc pp_lam (Array.to_list args) ++
-            str")")
   | Lproj(p,arg) ->
     hov 1
       (str "(proj " ++ Projection.Repr.print p ++ str "(" ++ pp_lam arg
@@ -566,7 +560,7 @@ let rec get_alias env kn =
 (* Compilation of primitive *)
 
 let prim kn p args =
-  Lprim(Some kn, p, args)
+  Lprim (kn, p, args)
 
 let expand_prim kn op arity =
   (* primitives are always Relevant *)
-- 
cgit v1.2.3