diff options
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 75d3ed30ba..2090aad8a0 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -160,9 +160,7 @@ 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.VarInstance _ -> - (* These are the two evar kinds used for existing goals *) - (* see Proofview.mark_in_evm *) + | Evar_kinds.GoalEvar -> PEvar (evk,Array.map (pattern_of_constr env) ctxt) | _ -> let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in |