From 9c91b2f49d1379d2c8ae43ff94fe4183ef4f8bf0 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sun, 14 Apr 2019 11:47:29 +0200
Subject: [native compiler] Remove `Lconstruct` from lambda code.

This is a step towards unifying the higher level ILs of the native and
bytecode compilers.

See https://github.com/coq/coq/projects/17
---
 kernel/nativecode.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'kernel/nativecode.ml')

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 94ed288d2d..ebb3c2cd73 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1280,9 +1280,6 @@ let ml_of_instance instance u =
   | Lmakeblock (prefix,(cn,_u),_,args) ->
      let args = Array.map (ml_of_lam env l) args in
      MLconstruct(prefix,cn,args)
-  | Lconstruct (prefix, (cn,u)) ->
-     let uargs = ml_of_instance env.env_univ u in
-      mkMLapp (MLglobal (Gconstruct (prefix, cn))) uargs
   | Luint i -> MLapp(MLprimitive Mk_uint, [|MLuint i|])
   | Lval v ->
       let i = push_symbol (SymbValue v) in get_value_code i
-- 
cgit v1.2.3