diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 11bb6b436..ab04ebaf6 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3417,7 +3417,7 @@ let admit_as_an_axiom gl = let concl = it_mkNamedProd_or_LetIn (pf_concl gl) sign in if occur_existential concl then error"\"admit\" cannot handle existentials."; let axiom = - let cd = Entries.ParameterEntry (concl,false) in + let cd = Entries.ParameterEntry (concl,None) in let con = Declare.declare_constant ~internal:Declare.KernelSilent na (cd,IsAssumption Logical) in constr_of_global (ConstRef con) in |