diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 10 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 3 | ||||
| -rw-r--r-- | vernac/vernacinterp.ml | 1 |
3 files changed, 8 insertions, 6 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..9ff4e33020 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2010,9 +2010,6 @@ let interp ?proof ~atts ~st c = | 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.") | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm.") 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 |