diff options
| author | Arnaud Spiwack | 2014-11-13 09:21:04 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-11-19 10:11:45 +0100 |
| commit | 7232e8f3fc5237705b80a870a6a3ad1a4748b838 (patch) | |
| tree | c4899325e80b1c6fc34c83bef5d27ed45bad2c2f | |
| parent | bd2dd62ea83ff9374bd28f089b19d3abba6ac7cb (diff) | |
uconstr: fix bug in interpretation of Ltac-bound name in let-tuple and pattern-matching.
In the syntax [let (x1,…,xn) := b in e] the name [x1…xn] were not interpreted with respect to the Ltac context. Hence typeable term would raise type-errors.
The same problem also existed in pattern-matching.
| -rw-r--r-- | pretyping/pretyping.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 71ed28c97d..f5aea567f4 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -711,6 +711,8 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var if not (Int.equal (List.length nal) cs.cs_nargs) then user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables."); + let nal = List.map (fun na -> ltac_interp_name lvar na) nal in + let na = ltac_interp_name lvar na in let fsign, record = match get_projections env indf with | None -> List.map2 (fun na (_,c,t) -> (na,c,t)) @@ -851,6 +853,9 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var inh_conv_coerce_to_tycon loc env evdref cj tycon | GCases (loc,sty,po,tml,eqns) -> + let (tml,eqns) = + Glob_ops.map_pattern_binders (fun na -> ltac_interp_name lvar na) tml eqns + in Cases.compile_cases loc sty ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref) tycon env (* loc *) (po,tml,eqns) |