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 /kernel/indtypes.ml | |
| 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 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 39455a7d2..45e0261d3 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -666,7 +666,8 @@ let compute_projections ((kn, _ as ind), u as indsp) n x nparamargs params let mp, dp, l = repr_mind kn in let rp = mkApp (mkIndU indsp, rel_vect 0 nparamargs) in let ci = - let print_info = { ind_nargs = 0; style = LetStyle } in + let print_info = + { ind_tags = []; cstr_tags = [|rel_context_tags ctx|]; style = LetStyle } in { ci_ind = ind; ci_npar = nparamargs; ci_cstr_ndecls = mind_consnrealdecls; |