diff options
| author | Pierre-Marie Pédrot | 2014-09-04 10:23:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-04 15:22:27 +0200 |
| commit | 3806d567af6b1feee2c8f196199eee4208a8551d (patch) | |
| tree | 5e6a7657058d52f18869c3bdfa618e5f7bb26b90 /pretyping/cases.ml | |
| parent | f3b714f5a8e516ee9731d705808a4084caae5a1e (diff) | |
Typing.sort_of does not leak evarmaps anymore.
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 737c9fa1b0..560289d1ee 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -2337,7 +2337,7 @@ let compile_program_cases loc style (typing_function, evdref) tycon env let pred = prepare_predicate_from_arsign_tycon loc tomatchs sign t in (* The tycon may be ill-typed after abstraction. *) let env' = push_rel_context (context_of_arsign sign) env in - ignore(Typing.sort_of env' !evdref pred); pred + ignore(Typing.sort_of env' evdref pred); pred with e when Errors.noncritical e -> let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in lift nar t |