diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/classes.ml | 4 | ||||
| -rw-r--r-- | vernac/topfmt.ml | 5 | ||||
| -rw-r--r-- | vernac/topfmt.mli | 1 |
3 files changed, 7 insertions, 3 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index ec01314e46..dd49f09d35 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -269,9 +269,9 @@ let do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode ct Pretyping.check_evars env (Evd.from_env env) sigma termtype; let termtype = to_constr sigma termtype in let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in - if not (Evd.has_undefined sigma) && not (Option.is_empty term) then + if not (Evd.has_undefined sigma) && not (Option.is_empty props) then declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype - else if program_mode || refine || Option.is_empty term then + else if program_mode || refine || Option.is_empty props then declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype else CErrors.user_err Pp.(str "Unsolved obligations remaining."); id diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index b4b893a3fd..ed93267665 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -335,6 +335,7 @@ type execution_phase = | LoadingPrelude | LoadingRcFile | InteractiveLoop + | CompilationPhase let default_phase = ref InteractiveLoop @@ -373,7 +374,9 @@ let pr_phase ?loc () = Some (str "While loading initial state:" ++ Option.cata (fun loc -> fnl () ++ pr_loc loc) (mt ()) loc) | _, Some loc -> Some (pr_loc loc) | ParsingCommandLine, _ - | Initialization, _ -> None + | Initialization, _ + | CompilationPhase, _ -> + None | InteractiveLoop, _ -> (* Note: interactive messages such as "foo is defined" are not located *) None diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 5f84c5edee..b0e3b3772c 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -60,6 +60,7 @@ type execution_phase = | LoadingPrelude | LoadingRcFile | InteractiveLoop + | CompilationPhase val in_phase : phase:execution_phase -> ('a -> 'b) -> 'a -> 'b |