diff options
| author | Arnaud Spiwack | 2014-12-19 09:00:25 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-12-19 16:27:45 +0100 |
| commit | a07648ca9c6b06414b271632c620122e51bf0f4a (patch) | |
| tree | 4bd1cceb919447c5397bca37d737503239226d7e | |
| parent | 7e63bd45b84f59d400065bffdd8af2f03d351a1b (diff) | |
When pretyping [uconstr] closures, don't use the local Ltac variable environment.
A closure is supposedly closed: all the relevant Ltac variables should be then. The last field [ltac_genargs], if I'm not mistaken, is there to represent the Ltac variables which are bound but not to something which makes sense in a term. They should be irrelevant at this point, since the uconstr has already been interpreted and these checks are supposed to have happened. (though I'm not entirely sure they do, it can be an interesting exercise to try and make [uconstr] behave weirdly)
I'm not quite sure why it caused #3679, though. But it still seems to be solved.
| -rw-r--r-- | pretyping/pretyping.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 07cc36815b..3957a40a68 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -304,10 +304,11 @@ let pretype_id pretype loc env evdref lvar id = { uj_val = c; uj_type = protected_get_type_of env sigma c } with Not_found -> try let {closure;term} = Id.Map.find id lvar.ltac_uconstrs in - let lvar = { lvar with + let lvar = { ltac_constrs = closure.typed; ltac_uconstrs = closure.untyped; - ltac_idents = closure.idents } + ltac_idents = closure.idents; + ltac_genargs = Id.Map.empty; } in (* spiwack: I'm catching [Not_found] potentially too eagerly here, as the call to the main pretyping function is caught |