diff options
Diffstat (limited to 'tactics/leminv.ml')
| -rw-r--r-- | tactics/leminv.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 5e5de2589..23a7c9e53 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -194,7 +194,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = errorlabstrm "lemma_inversion" (str"Computed inversion goal was not closed in initial signature."); *) - let pf = Proof.start Evd.empty [invEnv,invGoal] in + let pf = Proof.start Evd.empty [invEnv,(invGoal,get_universe_context_set sigma)] in let pf = fst (Proof.run_tactic env ( tclTHEN intro (onLastHypId inv_op)) pf) @@ -232,6 +232,9 @@ let add_inversion_lemma name env sigma t sort dep inv_op = const_entry_body = Future.from_val (invProof,Declareops.no_seff); const_entry_secctx = None; const_entry_type = None; + const_entry_proj = None; + const_entry_polymorphic = true; + const_entry_universes = Univ.UContext.empty (*FIXME *); const_entry_opaque = false; const_entry_inline_code = false; const_entry_feedback = None; @@ -244,8 +247,9 @@ let add_inversion_lemma name env sigma t sort dep inv_op = let add_inversion_lemma_exn na com comsort bool tac = let env = Global.env () and sigma = Evd.empty in - let c = Constrintern.interp_type sigma env com in - let sort = Pretyping.interp_sort comsort in + let c,ctx = Constrintern.interp_type sigma env com in + let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in + let sigma, sort = Pretyping.interp_sort sigma comsort in try add_inversion_lemma na env sigma c sort bool tac with @@ -260,7 +264,7 @@ let lemInv id c gls = try let clause = mk_clenv_type_of gls c in let clause = clenv_constrain_last_binding (mkVar id) clause in - Clenvtac.res_pf clause ~flags:Unification.elim_flags gls + Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) gls with | NoSuchBinding -> errorlabstrm "" |