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/nativelambda.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'kernel/nativelambda.mli') diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index b0de257a27..687789e82b 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -36,8 +36,6 @@ type lambda = | Lmakeblock of prefix * pconstructor * int * lambda array (* prefix, constructor Name.t, constructor tag, arguments *) (* A fully applied constructor *) - | Lconstruct of prefix * pconstructor (* prefix, constructor Name.t *) - (* A partially applied constructor *) | Luint of Uint63.t | Lval of Nativevalues.t | Lsort of Sorts.t -- cgit v1.2.3