diff options
| author | Matthieu Sozeau | 2015-04-09 17:32:36 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-04-09 17:32:36 +0200 |
| commit | f973052543cdd0f4c98366a7c2eefabeaf138afa (patch) | |
| tree | 73b8d12ea1b9eb82af552ca89715a2bd939a63db | |
| parent | b322c6131ab45be2d65ab2f6fcbcde7588314260 (diff) | |
Really fix constr_of_pattern and bugs #3590 and #4120 by
removing all evars appearing in the constr (or their types,
recursively) from the evar_map.
| -rw-r--r-- | pretyping/patternops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 9fb6ec9d11..705e594af1 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -167,13 +167,13 @@ let pattern_of_constr env sigma t = | Evar_kinds.MatchingVar (b,id) -> let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in ctx := (id,None,ty)::!ctx; - keep := Evar.Set.union (evars_of_term ty) !keep; + let () = ignore (pattern_of_constr env ty) in assert (not b); PMeta (Some id) | Evar_kinds.GoalEvar -> PEvar (evk,Array.map (pattern_of_constr env) ctxt) | _ -> let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in - remove := Evar.Set.union (evars_of_term ty) !remove; + let () = ignore (pattern_of_constr env ty) in PMeta None) | Case (ci,p,a,br) -> let cip = |