diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 7534214839..d12a65db61 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -187,7 +187,7 @@ let cook_proof () = and strength = ts.top_strength in let pfterm = extract_pftreestate pfs in (ident, - ({ const_entry_body = Cooked pfterm; const_entry_type = Some concl }, + ({ const_entry_body = pfterm; const_entry_type = Some concl }, strength)) (*********************************************************************) |