diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comInductive.ml | 2 | ||||
| -rw-r--r-- | vernac/declare.ml | 7 |
2 files changed, 6 insertions, 3 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 4242f06844..95489c9132 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -117,7 +117,7 @@ let intern_ind_arity env sigma ind = let pretype_ind_arity env sigma (loc, c, impls, pseudo_poly) = let sigma,t = understand_tcc env sigma ~expected_type:IsType c in match Reductionops.sort_of_arity env sigma t with - | exception Invalid_argument _ -> + | exception Reduction.NotArity -> user_err ?loc (str "Not an arity") | s -> let concl = match pseudo_poly with diff --git a/vernac/declare.ml b/vernac/declare.ml index 7de1ff4083..e3144b2d24 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -911,8 +911,11 @@ end (* Locality stuff *) let declare_entry_core ~name ~scope ~kind ?hook ~obls ~impargs ~uctx entry = - let should_suggest = entry.proof_entry_opaque && - Option.is_empty entry.proof_entry_secctx in + let should_suggest = + entry.proof_entry_opaque + && not (List.is_empty (Global.named_context())) + && Option.is_empty entry.proof_entry_secctx + in let ubind = UState.universe_binders uctx in let dref = match scope with | Discharge -> |