diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 10 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 30 | ||||
| -rw-r--r-- | vernac/vernacinterp.ml | 1 | ||||
| -rw-r--r-- | vernac/vernacprop.ml | 1 |
4 files changed, 18 insertions, 24 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 249e7893c2..698ee4703a 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -559,15 +559,21 @@ let rec explain_evar_kind env sigma evk ty = function | Evar_kinds.VarInstance id -> strbrk "an instance of type " ++ ty ++ str " for the variable " ++ Id.print id - | Evar_kinds.SubEvar evk' -> + | Evar_kinds.SubEvar (where,evk') -> let evi = Evd.find sigma evk' in let pc = match evi.evar_body with | Evar_defined c -> pr_leconstr_env env sigma (EConstr.of_constr c) | Evar_empty -> assert false in let ty' = EConstr.of_constr evi.evar_concl in + (match where with + | Some Evar_kinds.Body -> str "the body of " + | Some Evar_kinds.Domain -> str "the domain of " + | Some Evar_kinds.Codomain -> str "the codomain of " + | None -> pr_existential_key sigma evk ++ str " of type " ++ ty ++ str " in the partial instance " ++ pc ++ - str " found for " ++ explain_evar_kind env sigma evk' + str " found for ") ++ + explain_evar_kind env sigma evk' (pr_leconstr_env env sigma ty') (snd evi.evar_source) let explain_typeclass_resolution env sigma evi k = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 3dbe8b0c09..b44c7cccba 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,10 +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") - - (* Toplevel control *) - | VernacToplevelControl e -> raise e (* Resetting *) | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm.") @@ -2028,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 @@ -2102,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 @@ -2171,7 +2161,7 @@ let check_vernac_supports_locality c l = | VernacDeclareMLModule _ | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _ | VernacSyntacticDefinition _ - | VernacArgumentsScope _ | VernacDeclareImplicits _ | VernacArguments _ + | VernacArguments _ | VernacGeneralizable _ | VernacSetOpacity _ | VernacSetStrategy _ | VernacSetOption _ | VernacUnsetOption _ diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 1f2d2e4b42..d4f2a753ff 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -79,7 +79,6 @@ let call opn converted_args ~atts ~st = phase := "Executing command"; hunk ~atts ~st with - | Drop -> raise Drop | reraise -> let reraise = CErrors.push reraise in if !Flags.debug then diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml index a837b77a33..0fdd2faafa 100644 --- a/vernac/vernacprop.ml +++ b/vernac/vernacprop.ml @@ -31,7 +31,6 @@ let rec has_Fail = function let is_navigation_vernac_expr = function | VernacResetInitial | VernacResetName _ - | VernacBacktrack _ | VernacBackTo _ | VernacBack _ -> true | _ -> false |