diff options
| author | herbelin | 2000-05-16 12:17:13 +0000 |
|---|---|---|
| committer | herbelin | 2000-05-16 12:17:13 +0000 |
| commit | dc8fd42f1dd657ac503c8d2fd0ec7cd407b2e78e (patch) | |
| tree | cd9af1c454cccd00b050cbc343f386ae7121892f | |
| parent | 7fb4e6304a9af9125a49d109a13e6d2961d4e11b (diff) | |
Rien
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@432 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 5e91541ec3..5f789d7f89 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 |