diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/leminv.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 5e91541ec..5f789d7f8 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -218,10 +218,6 @@ let inversion_scheme env sigma t sort dep_option inv_op = let invProof = it_lambda_name env (local_strong (whd_meta mvb) pfterm) ownSign in invProof -(* -open Discharge -open Constrtypes -*) let add_inversion_lemma name env sigma t sort dep inv_op = let invProof = inversion_scheme env sigma t sort dep inv_op in @@ -261,7 +257,6 @@ let _ = inversion_lemma_from_goal n na id prop false inv_clear_tac | _ -> bad_vernac_args "MakeInversionLemmaFromHyp") - let add_inversion_lemma_exn na com comsort bool tac = let env = Global.env () and sigma = Evd.empty in let c = Astterm.interp_type sigma env com in |