diff options
| author | Hugo Herbelin | 2014-10-22 10:32:45 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-22 11:04:30 +0200 |
| commit | 2592ea6490cdf799432260c99a934605a2739849 (patch) | |
| tree | 11f8e09fd434270694090194eebe708cefdfef11 /pretyping | |
| parent | c25ff7718d77e4aba0827c4d45a507ed49db72e0 (diff) | |
Fixing an evar leak in pattern-matching compilation (#3758).
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 78837b9d8c..7da59b94e2 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -293,10 +293,13 @@ let try_find_ind env sigma typ realnames = IsInd (typ,ind,names) let inh_coerce_to_ind evdref env ty tyi = + let sigma = !evdref in let expected_typ = inductive_template evdref env None tyi in - (* devrait être indifférent d'exiger leq ou pas puisque pour - un inductif cela doit être égal *) - let _ = e_cumul env evdref expected_typ ty in () + (* Try to refine the type with inductive information coming from the + constructor and renounce if not able to give more information *) + (* devrait être indifférent d'exiger leq ou pas puisque pour + un inductif cela doit être égal *) + if not (e_cumul env evdref expected_typ ty) then evdref := sigma let binding_vars_of_inductive = function | NotInd _ -> [] |