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.
---
 interp/constrextern.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 8e6485b7bc..40e0901beb 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -999,7 +999,7 @@ let rec glob_of_pat env sigma = function
   | PIf (c,b1,b2) ->
       GIf (loc, glob_of_pat env sigma c, (Anonymous,None),
            glob_of_pat env sigma b1, glob_of_pat env sigma b2)
-  | PCase ({cip_style=LetStyle; cip_ind_args=None},PMeta None,tm,[(0,n,b)]) ->
+  | PCase ({cip_style=LetStyle; cip_ind_tags=None},PMeta None,tm,[(0,n,b)]) ->
       let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat env sigma b) in
       GLetTuple (loc,nal,(Anonymous,None),glob_of_pat env sigma tm,b)
   | PCase (info,p,tm,bl) ->
@@ -1012,7 +1012,7 @@ let rec glob_of_pat env sigma = function
       in
       let mat = if info.cip_extensible then mat @ [any_any_branch] else mat
       in
-      let indnames,rtn = match p, info.cip_ind, info.cip_ind_args with
+      let indnames,rtn = match p, info.cip_ind, info.cip_ind_tags with
 	| PMeta None, _, _ -> (Anonymous,None),None
 	| _, Some ind, Some nargs ->
 	  return_type_of_predicate ind nargs (glob_of_pat env sigma p)
-- 
cgit v1.2.3