diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-28 16:30:45 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-28 16:37:12 +0200 |
| commit | 68fb8e13c44c5ee95dbc9256b1d74c7c83303d2d (patch) | |
| tree | 9b464872424a3b0fd01181f1b85b05e0b7112d75 /pretyping/patternops.ml | |
| parent | 9a91a385b2562a0656edf8766f229dc8120b2675 (diff) | |
Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).
The fix follows an invariant enforced in proofview.ml on the kind of
evars that are goals or that occur in goals.
One day, evar kinds will need a little cleaning...
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 2090aad8a..75d3ed30b 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -160,7 +160,9 @@ let pattern_of_constr env sigma t = let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in let () = ignore (pattern_of_constr env ty) in assert (not b); PMeta (Some id) - | Evar_kinds.GoalEvar -> + | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ -> + (* These are the two evar kinds used for existing goals *) + (* see Proofview.mark_in_evm *) PEvar (evk,Array.map (pattern_of_constr env) ctxt) | _ -> let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in |