diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-20 12:56:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-20 23:29:19 +0200 |
| commit | 7efeff178470ab204e531cd07176091bf5022da6 (patch) | |
| tree | afdc79d6eb2a371fa2cec235aabea3c5425d46b9 /interp | |
| parent | f00f8482e1d21ef8b03044ed2162cb29d9e4537d (diff) | |
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.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 8e6485b7b..40e0901be 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) |