From 4a84969d8f7faffef19a0da71bfccedc437daf5d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 14 Feb 2001 16:22:36 +0000
Subject: Erreur sur commit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1389 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/command.ml | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 5a029a0e67..49dd7b8873 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -440,11 +440,8 @@ let save opacity id ({const_entry_body = pft; const_entry_type = tpo} as const)
   strength =
   begin match strength with
     | DischargeAt disch_sp when Lib.is_section_p disch_sp ->
-	(*
 	let c = constr_of_constr_entry const in
 	let _ = declare_variable id (SectionLocalDef c,strength,opacity) in ()
-	*)
-        let _ = declare_constant id (ConstantEntry const,strength,opacity)in ()
     | NeverDischarge | DischargeAt _ ->
         let _ = declare_constant id (ConstantEntry const,strength,opacity)in ()
     | NotDeclare -> apply_tac_not_declare id pft tpo
-- 
cgit v1.2.3