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.ml | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'kernel/context.ml') diff --git a/kernel/context.ml b/kernel/context.ml index 5256ee417..5cb964b9c 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -76,6 +76,13 @@ let rel_context_nhyps hyps = | (_,Some _,_)::hyps -> nhyps acc hyps in nhyps 0 hyps +let rel_context_tags ctx = + let rec aux l = function + | [] -> l + | (_,Some _,_)::ctx -> aux (true::l) ctx + | (_,None _,_)::ctx -> aux (false::l) ctx + in aux [] ctx + (*s Signatures of named hypotheses. Used for section variables and goal assumptions. *) -- cgit v1.2.3