diff options
| author | Matthieu Sozeau | 2014-06-24 17:27:24 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-24 18:53:52 +0200 |
| commit | ff2da62916d9a6bec4aae1a576ce5d396ea9893e (patch) | |
| tree | cc545ccac688a4283f08989563387d763f22b4de /pretyping | |
| parent | 9f1f8e29baa6d8f8d458740737d0fbd02de31c6c (diff) | |
Fix program cases and inversion tactic to correctly record universe constraints.
Fixes FingerTree contrib.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index b5aeeae3ab..50396d8547 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -2155,6 +2155,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels' and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in + let _btype = evd_comb1 (Typing.e_type_of env) evdref bbody in let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in let branch = |