diff options
| author | filliatr | 1999-12-09 15:10:08 +0000 |
|---|---|---|
| committer | filliatr | 1999-12-09 15:10:08 +0000 |
| commit | a4436a6a355ecb3fffb52d1ca3f2d983a5bcfefd (patch) | |
| tree | 0252d3bb7d7f9c55dad753f39e83de5efba41de4 /proofs | |
| parent | f09ca438e24bc4016b4e778dd8fd4de4641b7636 (diff) | |
- 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
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 9 |
1 files changed, 6 insertions, 3 deletions
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") |