From a4436a6a355ecb3fffb52d1ca3f2d983a5bcfefd Mon Sep 17 00:00:00 2001
From: filliatr
Date: Thu, 9 Dec 1999 15:10:08 +0000
Subject:  - constantes avec recettes  - discharge en deux temps, avec état
 remis comme au début de la section (mais c'est toujours buggé)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@224 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/pfedit.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 12f53c685d..e2f5ce94b4 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -175,7 +175,8 @@ let save_named opacity =
   and strength = ts.top_strength in
   let pfterm = extract_pftreestate pfs in 
   declare_constant (id_of_string ident)
-    ({ const_entry_body = pfterm; const_entry_type = Some concl }, strength);
+    ({ const_entry_body = Cooked pfterm; const_entry_type = Some concl }, 
+     strength);
   del_proof ident;
   message(ident ^ " is defined")
     
@@ -187,11 +188,13 @@ let save_anonymous opacity save_ident n =
   let pfterm = extract_pftreestate pfs in 
   if ident = "Unnamed_thm" then
     declare_constant (id_of_string save_ident)
-      ({ const_entry_body = pfterm; const_entry_type = Some concl }, strength)
+      ({ const_entry_body = Cooked pfterm; const_entry_type = Some concl }, 
+       strength)
   else begin
     message("Overriding name " ^ ident ^ " and using " ^ save_ident);
     declare_constant (id_of_string save_ident)
-      ({ const_entry_body = pfterm; const_entry_type = Some concl }, strength)
+      ({ const_entry_body = Cooked pfterm; const_entry_type = Some concl }, 
+       strength)
   end;
   del_proof ident;
   message(save_ident ^ " is defined")
-- 
cgit v1.2.3