From 72c03f36e2e969992acf8e0398bbf7ae2c2c70b8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 20 Nov 2001 15:35:22 +0000
Subject: Fusion de declare/add_constant, declare/add_parameter et
 add_discharged_constant

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2211 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/setoid_replace.ml | 18 +++++++++---------
 tactics/tactics.ml        |  5 +++--
 2 files changed, 12 insertions(+), 11 deletions(-)

(limited to 'tactics')

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index f83436e160..0f1b749a62 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -234,14 +234,14 @@ let add_setoid a aeq th =
 	    let eq_ext_name = gen_eq_lem_name () in 
 	    let eq_ext_name2 = gen_eq_lem_name () in 
 	    let _ = Declare.declare_constant eq_ext_name
-		      ((Declare.ConstantEntry {const_entry_body = eq_morph; 
-					       const_entry_type = None;
-                                               const_entry_opaque = true}),
+		      ((ConstantEntry {const_entry_body = eq_morph; 
+				       const_entry_type = None;
+                                       const_entry_opaque = true}),
 		       Declare.NeverDischarge) in
 	    let _ = Declare.declare_constant eq_ext_name2
-		      ((Declare.ConstantEntry {const_entry_body = eq_morph2; 
-					       const_entry_type = None;
-                                               const_entry_opaque = true}),
+		      ((ConstantEntry {const_entry_body = eq_morph2; 
+				       const_entry_type = None;
+                                       const_entry_opaque = true}),
 		       Declare.NeverDischarge) in
 	    let eqmorph = (current_constant eq_ext_name) in
 	    let eqmorph2 = (current_constant eq_ext_name2) in
@@ -459,9 +459,9 @@ let add_morphism lem_name (m,profil) =
 	 (let lem_2 = gen_lem_iff env m mext args_t poss in
 	  let lem2_name = add_suffix lem_name "2" in
 	  let _ = Declare.declare_constant lem2_name
-		    ((Declare.ConstantEntry {const_entry_body = lem_2; 
-					     const_entry_type = None;
-                                               const_entry_opaque = true}),
+		    ((ConstantEntry {const_entry_body = lem_2; 
+				     const_entry_type = None;
+                                     const_entry_opaque = true}),
 		     Declare.NeverDischarge) in
 	  let lem2 = (current_constant lem2_name) in
 	    (Lib.add_anonymous_leaf
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e7d61a79a5..dc87c10f2c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -422,7 +422,7 @@ let hide_ident_or_numarg_tactic s tac =
    | _ -> assert false in
   add_tactic s tacfun;
   fun id -> vernac_tactic(s,[Identifier id])
-      
+
 
 (* Obsolete, remplace par intros_unitl_n ?
 let intros_do n g = 
@@ -1844,7 +1844,8 @@ let abstract_subproof name tac gls =
       with e when catchable_exception e -> 
 	(delete_current_proof(); raise e)
     in   (* Faudrait un peu fonctionnaliser cela *)
-    let sp = Declare.declare_constant na (ConstantEntry const,strength) in
+    let cd = Safe_typing.ConstantEntry const in
+    let sp = Declare.declare_constant na (cd,strength) in
     let newenv = Global.env() in
     Declare.constr_of_reference (ConstRef sp)
   in
-- 
cgit v1.2.3