From 723c344d3e4cf7fdc2e4854ea7d55d140570424d Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 6 Nov 2000 16:43:51 +0000
Subject: nouveau discharge fait par le noyau; plus de recettes dans les corps
 des constantes

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

(limited to 'tactics')

diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index d562b0ed90..9290fd5a1c 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -231,7 +231,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
 let add_inversion_lemma name env sigma t sort dep inv_op =
   let invProof = inversion_scheme env sigma t sort dep inv_op in
   declare_constant name
-    ({ const_entry_body = Cooked invProof; const_entry_type = None }, 
+    (ConstantEntry { const_entry_body = invProof; const_entry_type = None }, 
      NeverDischarge)
 
 (* open Pfedit *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8b9a8d0af1..20bed0eab6 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1663,7 +1663,7 @@ let abstract_subproof name tac gls =
       with e when catchable_exception e -> 
 	(delete_current_proof(); raise e)
     in   (* Faudrait un peu fonctionnaliser cela *)
-    Declare.declare_constant na (const,strength);
+    Declare.declare_constant na (ConstantEntry const,strength);
     let newenv = Global.env() in
     Declare.construct_reference newenv CCI na
   in
-- 
cgit v1.2.3