diff options
Diffstat (limited to 'vernac')
67 files changed, 112 insertions, 144 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 9353ef3902..d7cb9dc727 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -168,7 +168,7 @@ let rec traverse current ctx accu t = match Constr.kind t with let body () = id |> Global.lookup_named |> NamedDecl.get_value in traverse_object accu body (VarRef id) | Const (kn, _) -> - let body () = Option.map fst (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in + let body () = Option.map pi1 (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in traverse_object accu body (ConstRef kn) | Ind ((mind, _) as ind, _) -> traverse_inductive accu mind (IndRef ind) @@ -181,7 +181,7 @@ let rec traverse current ctx accu t = match Constr.kind t with | Lambda(_,_,oty), Const (kn, _) when Vars.noccurn 1 oty && not (Declareops.constant_has_body (lookup_constant kn)) -> - let body () = Option.map fst (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in + let body () = Option.map pi1 (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in traverse_object ~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn) | _ -> diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli index 536185f4aa..5e63829411 100644 --- a/vernac/assumptions.mli +++ b/vernac/assumptions.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/attributes.ml b/vernac/attributes.ml index ab14974598..6af454eee5 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 53caf49efd..34ff15ca7d 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 2e84c3275b..38852992e4 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/auto_ind_decl.mli b/vernac/auto_ind_decl.mli index 647ff3d8d6..0de8c61f59 100644 --- a/vernac/auto_ind_decl.mli +++ b/vernac/auto_ind_decl.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/canonical.ml b/vernac/canonical.ml index 92d5731f92..e9454bab8a 100644 --- a/vernac/canonical.ml +++ b/vernac/canonical.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/canonical.mli b/vernac/canonical.mli index 5b223a0615..a3bbaf6d18 100644 --- a/vernac/canonical.mli +++ b/vernac/canonical.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/class.ml b/vernac/class.ml index eed7107b39..420baf7966 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/class.mli b/vernac/class.mli index 85266739ad..d530d218d4 100644 --- a/vernac/class.mli +++ b/vernac/class.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/classes.ml b/vernac/classes.ml index 74903d196f..442f139827 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -281,9 +281,6 @@ let existing_instance glob g info = ~hdr:"declare_instance" (Pp.str "Constant does not build instances of a declared type class.") -let mismatched_params env n m = Implicit_quantifiers.mismatched_ctx_inst_err env Parameters n m -let mismatched_props env n m = Implicit_quantifiers.mismatched_ctx_inst_err env Properties n m - (* Declare everything in the parameters as implicit, and the class instance as well *) let type_ctx_instance ~program_mode env sigma ctx inst subst = @@ -479,9 +476,8 @@ let do_instance_interactive env sigma ?hook ~tac ~global ~poly cty k u ctx ctx' let do_instance env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id props = let term, termtype, sigma = match props with - | (true, { CAst.v = CRecord fs }) -> - if List.length fs > List.length k.cl_props then - mismatched_props env' (List.map snd fs) k.cl_props; + | (true, { CAst.v = CRecord fs; loc }) -> + check_duplicate ?loc fs; let subst, sigma = do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode:false subst in let term, termtype = do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in @@ -502,9 +498,8 @@ let do_instance env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imp let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props = let term, termtype, sigma = match opt_props with - | Some (true, { CAst.v = CRecord fs }) -> - if List.length fs > List.length k.cl_props then - mismatched_props env' (List.map snd fs) k.cl_props; + | Some (true, { CAst.v = CRecord fs; loc }) -> + check_duplicate ?loc fs; let subst, sigma = do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode:true subst in let term, termtype = diff --git a/vernac/classes.mli b/vernac/classes.mli index ace9096469..472690cdd4 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -14,12 +14,6 @@ open Constrexpr open Typeclasses open Libnames -(** Errors *) - -val mismatched_params : env -> constr_expr list -> Constr.rel_context -> 'a - -val mismatched_props : env -> constr_expr list -> Constr.rel_context -> 'a - (** Instance declaration *) val declare_instance : ?warn:bool -> env -> Evd.evar_map -> diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index a27c08d176..3eb5eacd46 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 8f37bc0ba4..07e96d87a2 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index ae1f55acda..853f2c9aa3 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index cf309d6bbd..af09a83f02 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 0d7ba69955..a88413cf7f 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index ea9ab33346..b42e877d41 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 2f8b12f4c5..363ba5beff 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 224cce67ad..2d6ecf48ef 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 3bb9b0f6a1..23c98c97f9 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index f80884c124..42327d6bdd 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 5b656a2f5a..6f9608f04a 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 9bc225475d..c9d9b65e04 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/egramcoq.mli b/vernac/egramcoq.mli index 3a6f8ae015..f879d51660 100644 --- a/vernac/egramcoq.mli +++ b/vernac/egramcoq.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/egramml.ml b/vernac/egramml.ml index bc58993a2e..62eb561f3c 100644 --- a/vernac/egramml.ml +++ b/vernac/egramml.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/egramml.mli b/vernac/egramml.mli index 1cf75a55b1..1fe2395df2 100644 --- a/vernac/egramml.mli +++ b/vernac/egramml.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index 2bc95dbfcd..5c5a4ffbcb 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -44,59 +44,61 @@ let explain_exn_default = function let _ = CErrors.register_handler explain_exn_default -(** Pre-explain a vernac interpretation error *) - -let wrap_vernac_error (exn, info) strm = (EvaluatedError (strm, None), info) - -let process_vernac_interp_error exn = match fst exn with +let vernac_interp_error_handler = function | Univ.UniverseInconsistency i -> let msg = if !Constrextern.print_universes then - str "." ++ spc() ++ - Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i + str "." ++ spc() ++ + Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i else mt() in - wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".") + str "Universe inconsistency" ++ msg ++ str "." | TypeError(ctx,te) -> - let te = map_ptype_error EConstr.of_constr te in - wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te) + let te = map_ptype_error EConstr.of_constr te in + Himsg.explain_type_error ctx Evd.empty te | PretypeError(ctx,sigma,te) -> - wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te) + Himsg.explain_pretype_error ctx sigma te | Notation.PrimTokenNotationError(kind,ctx,sigma,te) -> - wrap_vernac_error exn (Himsg.explain_prim_token_notation_error kind ctx sigma te) + Himsg.explain_prim_token_notation_error kind ctx sigma te | Typeclasses_errors.TypeClassError(env, sigma, te) -> - wrap_vernac_error exn (Himsg.explain_typeclass_error env sigma te) - | Implicit_quantifiers.MismatchedContextInstance(e,c,l,x) -> - wrap_vernac_error exn (Himsg.explain_mismatched_contexts e c l x) + Himsg.explain_typeclass_error env sigma te | InductiveError e -> - wrap_vernac_error exn (Himsg.explain_inductive_error e) + Himsg.explain_inductive_error e | Modops.ModuleTypingError e -> - wrap_vernac_error exn (Himsg.explain_module_error e) + Himsg.explain_module_error e | Modintern.ModuleInternalizationError e -> - wrap_vernac_error exn (Himsg.explain_module_internalization_error e) + Himsg.explain_module_internalization_error e | RecursionSchemeError (env,e) -> - wrap_vernac_error exn (Himsg.explain_recursion_scheme_error env e) + Himsg.explain_recursion_scheme_error env e | Cases.PatternMatchingError (env,sigma,e) -> - wrap_vernac_error exn (Himsg.explain_pattern_matching_error env sigma e) + Himsg.explain_pattern_matching_error env sigma e | Tacred.ReductionTacticError e -> - wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e) + Himsg.explain_reduction_tactic_error e | Logic.RefinerError (env, sigma, e) -> - wrap_vernac_error exn (Himsg.explain_refiner_error env sigma e) + Himsg.explain_refiner_error env sigma e | Nametab.GlobalizationError q -> - wrap_vernac_error exn - (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++ - spc () ++ str "was not found" ++ - spc () ++ str "in the current" ++ spc () ++ str "environment.") + str "The reference" ++ spc () ++ Libnames.pr_qualid q ++ + spc () ++ str "was not found" ++ + spc () ++ str "in the current" ++ spc () ++ str "environment." | Refiner.FailError (i,s) -> - let s = Lazy.force s in - wrap_vernac_error exn - (str "Tactic failure" ++ - (if Pp.ismt s then s else str ": " ++ s) ++ - if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").") + let s = Lazy.force s in + str "Tactic failure" ++ + (if Pp.ismt s then s else str ": " ++ s) ++ + if Int.equal i 0 then str "." else str " (level " ++ int i ++ str")." | AlreadyDeclared msg -> - wrap_vernac_error exn (msg ++ str ".") + msg ++ str "." | _ -> - exn + raise CErrors.Unhandled + +let _ = CErrors.register_handler vernac_interp_error_handler + +(** Pre-explain a vernac interpretation error *) + +let wrap_vernac_error (exn, info) strm = (EvaluatedError (strm, None), info) + +let process_vernac_interp_error exn = + try vernac_interp_error_handler (fst exn) |> wrap_vernac_error exn + with CErrors.Unhandled -> exn let rec strip_wrapping_exceptions = function | Logic_monad.TacticFailure e -> @@ -108,16 +110,9 @@ let additional_error_info = ref [] let register_additional_error_info f = additional_error_info := f :: !additional_error_info -let process_vernac_interp_error ?(allow_uncaught=true) (exc, info) = +let process_vernac_interp_error (exc, info) = let exc = strip_wrapping_exceptions exc in let e = process_vernac_interp_error (exc, info) in - let () = - if not allow_uncaught && not (CErrors.handled (fst e)) then - let (e, info) = e in - let msg = str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "." in - let err = CErrors.make_anomaly msg in - Util.iraise (err, info) - in let e' = try Some (CList.find_map (fun f -> f e) !additional_error_info) with _ -> None diff --git a/vernac/explainErr.mli b/vernac/explainErr.mli index b54912a144..cc2a130925 100644 --- a/vernac/explainErr.mli +++ b/vernac/explainErr.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -13,7 +13,7 @@ exception EvaluatedError of Pp.t * exn option (** Pre-explain a vernac interpretation error *) -val process_vernac_interp_error : ?allow_uncaught:bool -> Util.iexn -> Util.iexn +val process_vernac_interp_error : Util.iexn -> Util.iexn (** General explain function. Should not be used directly now, see instead function [Errors.print] and variants *) diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index ea35ea782d..94876d2142 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index cec68b89bc..74bd552459 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/himsg.ml b/vernac/himsg.ml index a1f7835cbe..2e218942cb 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -1095,19 +1095,6 @@ let explain_unbound_method env sigma cid { CAst.v = id } = str "Unbound method name " ++ Id.print (id) ++ spc () ++ str"of class" ++ spc () ++ pr_global cid ++ str "." -let pr_constr_exprs env sigma exprs = - hv 0 (List.fold_right - (fun d pps -> ws 2 ++ Ppconstr.pr_constr_expr env sigma d ++ pps) - exprs (mt ())) - -let explain_mismatched_contexts env c i j = - let sigma = Evd.from_env env in - let pm, pn = with_diffs (pr_rel_context env sigma j) (pr_constr_exprs env sigma i) in - str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++ - hov 1 (str"Expected:" ++ brk (1, 1) ++ pm) ++ - fnl () ++ brk (1,1) ++ - hov 1 (str"Found:" ++ brk (1, 1) ++ pn) - let explain_typeclass_error env sigma = function | NotAClass c -> explain_not_a_class env sigma c | UnboundMethod (cid, id) -> explain_unbound_method env sigma cid id diff --git a/vernac/himsg.mli b/vernac/himsg.mli index d1c1c092e3..6458fb9e30 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -24,8 +24,6 @@ val explain_pretype_error : env -> Evd.evar_map -> pretype_error -> Pp.t val explain_inductive_error : inductive_error -> Pp.t -val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Constr.rel_context -> Pp.t - val explain_typeclass_error : env -> Evd.evar_map -> typeclass_error -> Pp.t val explain_recursion_scheme_error : env -> recursion_scheme_error -> Pp.t diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index f18cf17bf9..80b3df84db 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli index ebfc76de9d..a747ac6598 100644 --- a/vernac/indschemes.mli +++ b/vernac/indschemes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 2b204cb3de..400e0dfa3e 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -98,7 +98,7 @@ let retrieve_first_recthm uctx = function (* we get the right order somehow but surely it could be enforced in a better way *) let uctx = UState.context uctx in let inst = Univ.UContext.instance uctx in - let map (c, ctx) = Vars.subst_instance_constr inst c in + let map (c, _, _) = Vars.subst_instance_constr inst c in (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), is_opaque cb) | _ -> assert false diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index c5903bc874..70c8b511a1 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml index f5e8b6d12f..bea0c943c3 100644 --- a/vernac/loadpath.ml +++ b/vernac/loadpath.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/loadpath.mli b/vernac/loadpath.mli index 6605daa8d2..47d2d34125 100644 --- a/vernac/loadpath.mli +++ b/vernac/loadpath.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/locality.ml b/vernac/locality.ml index 465f04bc6e..bc33d53594 100644 --- a/vernac/locality.ml +++ b/vernac/locality.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/locality.mli b/vernac/locality.mli index 3c63c82117..be7e0cbe76 100644 --- a/vernac/locality.mli +++ b/vernac/locality.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index b96f500beb..90892feb13 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index 6532cee367..44e08c4819 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/mltop.ml b/vernac/mltop.ml index bbee9988d0..0130de2543 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/mltop.mli b/vernac/mltop.mli index b457c9c88f..56a28b64b0 100644 --- a/vernac/mltop.mli +++ b/vernac/mltop.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 87da73c534..a0010a5026 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index fda1e2afea..4f053b98ae 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/ppvernac.mli b/vernac/ppvernac.mli index 4aa24bf5db..d4d49a09a3 100644 --- a/vernac/ppvernac.mli +++ b/vernac/ppvernac.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index 1d089d0a55..094e2c1184 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/proof_using.mli b/vernac/proof_using.mli index 702043a4a9..a0567eef47 100644 --- a/vernac/proof_using.mli +++ b/vernac/proof_using.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index 4d9157089c..da28e260b3 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli index 41a2e7fd6f..c9eb979a90 100644 --- a/vernac/pvernac.mli +++ b/vernac/pvernac.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/record.ml b/vernac/record.ml index 48cde133a8..7cc8d9e9b9 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/record.mli b/vernac/record.mli index 24bb27e107..11d9a833e2 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/search.ml b/vernac/search.ml index a5663d65ef..d9ab76b11b 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/search.mli b/vernac/search.mli index 0f94ddc5b6..029e8cf7b9 100644 --- a/vernac/search.mli +++ b/vernac/search.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index bf2efb2542..7644f4c5b6 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 3d522a9e0f..dc4642dc65 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index bf57866d95..222f727f8e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -2308,8 +2308,7 @@ let with_fail ~st f = | HasNotFailed as e -> raise e | e when CErrors.noncritical e || e = Timeout -> let e = CErrors.push e in - raise (HasFailed (CErrors.iprint - (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e))) + raise (HasFailed (CErrors.iprint (ExplainErr.process_vernac_interp_error e))) with e when CErrors.noncritical e -> (* Restore the previous state XXX Careful here with the cache! *) Vernacstate.invalidate_cache (); diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 2895d0e4df..e46212ca1c 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index b8946fad23..6a67a49d0a 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index c7008c2a84..2725516a76 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index fd59d77237..3df74e5f2c 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml index b3490c7dc6..1dd8164ebc 100644 --- a/vernac/vernacprop.ml +++ b/vernac/vernacprop.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/vernacprop.mli b/vernac/vernacprop.mli index 8296a039f9..8875b86d94 100644 --- a/vernac/vernacprop.mli +++ b/vernac/vernacprop.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index c387c5c5f1..2bc20a747d 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index b78b252579..7e4d5d0315 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) |