aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/vernacentries.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/vernacentries.ml')
-rw-r--r--vernac/vernacentries.ml27
1 files changed, 10 insertions, 17 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 9ff4e3302..b44c7cccb 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -534,17 +534,14 @@ let vernac_assumption ~atts discharge kind l nl =
if not status then Feedback.feedback Feedback.AddedAxiom
let should_treat_as_cumulative cum poly =
- if poly then
- match cum with
- | GlobalCumulativity | LocalCumulativity -> true
- | GlobalNonCumulativity | LocalNonCumulativity -> false
- else
- match cum with
- | GlobalCumulativity | GlobalNonCumulativity -> false
- | LocalCumulativity ->
- user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.")
- | LocalNonCumulativity ->
- user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.")
+ match cum with
+ | Some VernacCumulative ->
+ if poly then true
+ else user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.")
+ | Some VernacNonCumulative ->
+ if poly then false
+ else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.")
+ | None -> poly && Flags.is_polymorphic_inductive_cumulativity ()
let vernac_record cum k poly finite struc binders sort nameopt cfs =
let is_cumulative = should_treat_as_cumulative cum poly in
@@ -565,7 +562,6 @@ let vernac_record cum k poly finite struc binders sort nameopt cfs =
indicates whether the type is inductive, co-inductive or
neither. *)
let vernac_inductive ~atts cum lo finite indl =
- let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in
if Dumpglob.dump () then
List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) ->
match cstrs with
@@ -602,6 +598,7 @@ let vernac_inductive ~atts cum lo finite indl =
| _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.")
in
let indl = List.map unpack indl in
+ let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in
ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo finite
let vernac_fixpoint ~atts discharge l =
@@ -2008,7 +2005,6 @@ let interp ?proof ~atts ~st c =
| VernacRestart -> CErrors.user_err (str "Restart cannot be used through the Load command")
| VernacUndo _ -> CErrors.user_err (str "Undo cannot be used through the Load command")
| VernacUndoTo _ -> CErrors.user_err (str "UndoTo cannot be used through the Load command")
- | VernacBacktrack _ -> CErrors.user_err (str "Backtrack cannot be used through the Load command")
(* Resetting *)
| VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm.")
@@ -2025,7 +2021,6 @@ let interp ?proof ~atts ~st c =
| VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
| VernacBindScope (sc,rl) -> vernac_bind_scope sc rl
| VernacOpenCloseScope (b, s) -> vernac_open_close_scope ~atts (b,s)
- | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope ~atts qid scl
| VernacInfix (mv,qid,sc) -> vernac_infix ~atts mv qid sc
| VernacNotation (c,infpl,sc) ->
vernac_notation ~atts c infpl sc
@@ -2099,8 +2094,6 @@ let interp ?proof ~atts ~st c =
vernac_hints ~atts dbnames hints
| VernacSyntacticDefinition (id,c,b) ->
vernac_syntactic_definition ~atts id c b
- | VernacDeclareImplicits (qid,l) ->
- vernac_declare_implicits ~atts qid l
| VernacArguments (qid, args, more_implicits, nargs, flags) ->
vernac_arguments ~atts qid args more_implicits nargs flags
| VernacReserve bl -> vernac_reserve bl
@@ -2168,7 +2161,7 @@ let check_vernac_supports_locality c l =
| VernacDeclareMLModule _
| VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _
| VernacSyntacticDefinition _
- | VernacArgumentsScope _ | VernacDeclareImplicits _ | VernacArguments _
+ | VernacArguments _
| VernacGeneralizable _
| VernacSetOpacity _ | VernacSetStrategy _
| VernacSetOption _ | VernacUnsetOption _