diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-06-24 17:27:24 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-24 18:53:52 +0200 |
| commit | ff2da62916d9a6bec4aae1a576ce5d396ea9893e (patch) | |
| tree | cc545ccac688a4283f08989563387d763f22b4de /tactics/inv.ml | |
| parent | 9f1f8e29baa6d8f8d458740737d0fbd02de31c6c (diff) | |
Fix program cases and inversion tactic to correctly record universe constraints.
Fixes FingerTree contrib.
Diffstat (limited to 'tactics/inv.ml')
| -rw-r--r-- | tactics/inv.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index dc8879521..ee875ce27 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -74,7 +74,7 @@ let make_inv_predicate env evd indf realargs id status concl = | NoDep -> (* We push the arity and leave concl unchanged *) let hyps_arity,_ = get_arity env indf in - (hyps_arity,concl) + (hyps_arity,concl) | Dep dflt_concl -> if not (occur_var env id concl) then errorlabstrm "make_inv_predicate" @@ -129,6 +129,7 @@ let make_inv_predicate env evd indf realargs id status concl = in let (newconcl, args) = build_concl [] [] 0 realargs in let predicate = it_mkLambda_or_LetIn_name env newconcl hyps in + let _ = Evarutil.evd_comb1 (Typing.e_type_of env) evd predicate in (* OK - this predicate should now be usable by res_elimination_then to do elimination on the conclusion. *) predicate, args |