From dc8fd42f1dd657ac503c8d2fd0ec7cd407b2e78e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 16 May 2000 12:17:13 +0000
Subject: Rien

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@432 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/leminv.ml | 5 -----
 1 file changed, 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
-- 
cgit v1.2.3