From 7efeff178470ab204e531cd07176091bf5022da6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 20 Oct 2014 12:56:43 +0200
Subject: A patch for printing "match" when constructors are defined with
 let-in but the internal representation dropped let-in.

Ideally, the internal representation of the "match" should use
contexts for the predicate and the branches. This would however be a
rather significant change. In the meantime, just a hack.

To do, there is still an extra @ in the constructor name that does not
need to be there.
---
 kernel/context.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel/context.mli')

diff --git a/kernel/context.mli b/kernel/context.mli
index 1d732d2732..b7eb7a76a3 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -115,3 +115,5 @@ val lookup_rel : int -> rel_context -> rel_declaration
 val rel_context_length : rel_context -> int
 (** Size of the [rel_context] without LetIns *)
 val rel_context_nhyps : rel_context -> int
+(** Indicates whether a LetIn or a Lambda, starting from oldest declaration *)
+val rel_context_tags : rel_context -> bool list
-- 
cgit v1.2.3