diff options
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 6dad04c98..f2642fcd1 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -692,7 +692,8 @@ let admit () = if k <> IsGlobal (Proof Conjecture) then error "Only statements declared as conjecture can be admitted"; *) - let (_,kn) = declare_constant id (ParameterEntry typ, IsConjecture) in + let (_,kn) = + declare_constant id (ParameterEntry typ, IsAssumption Conjectural) in hook Global (ConstRef kn); Pfedit.delete_current_proof (); assumption_message id |