diff options
| author | Maxime Dénès | 2013-12-29 10:53:06 -0500 |
|---|---|---|
| committer | Maxime Dénès | 2013-12-29 11:04:25 -0500 |
| commit | 381b2c6e77cd204aa143192a5a65e8832ae0633b (patch) | |
| tree | 2f26dca0d8085664d9bffde2c0dde5939c456b84 /kernel/nativelambda.ml | |
| parent | 651094ccfd2d8106a8b0e75c27dc89afb369d4b3 (diff) | |
Got rid of unused lazy flag in the native compiler.
Diffstat (limited to 'kernel/nativelambda.ml')
| -rw-r--r-- | kernel/nativelambda.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 7e46a05503..800c8e5fb1 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -14,7 +14,6 @@ open Pre_env open Nativevalues (** This file defines the lambda code generation phase of the native compiler *) - type lambda = | Lrel of name * int | Lvar of identifier @@ -90,15 +89,15 @@ let get_mind_prefix env mind = let _,name = lookup_mind_key mind env in match !name with | NotLinked -> "" - | Linked (s,_) -> s - | LinkedInteractive (s,_) -> s + | Linked s -> s + | LinkedInteractive s -> s let get_const_prefix env c = let _,(nameref,_) = lookup_constant_key c env in match !nameref with | NotLinked -> "" - | Linked (s,_) -> s - | LinkedInteractive (s,_) -> s + | Linked s -> s + | LinkedInteractive s -> s (* A generic map function *) |