diff options
Diffstat (limited to 'engine')
36 files changed, 214 insertions, 180 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 150dad16c2..4508633858 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -119,6 +119,20 @@ let isVarId sigma id c = let isRelN sigma n c = match kind sigma c with Rel n' -> Int.equal n n' | _ -> false +let isRef sigma c = match kind sigma c with + | Const _ | Ind _ | Construct _ | Var _ -> true + | _ -> false + +let isRefX sigma x c = + let open GlobRef in + match x, kind sigma c with + | ConstRef c, Const (c', _) -> Constant.equal c c' + | IndRef i, Ind (i', _) -> eq_ind i i' + | ConstructRef i, Construct (i', _) -> eq_constructor i i' + | VarRef id, Var id' -> Id.equal id id' + | _ -> false + + let destRel sigma c = match kind sigma c with | Rel p -> p | _ -> raise DestKO @@ -723,8 +737,27 @@ let fresh_global ?loc ?rigid ?names env sigma reference = let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in evd, t -let is_global sigma gr c = - Globnames.is_global gr (to_constr sigma c) +let is_global = isRefX + +(** Kind of type *) + +type kind_of_type = + | SortType of ESorts.t + | CastType of types * t + | ProdType of Name.t Context.binder_annot * t * t + | LetInType of Name.t Context.binder_annot * t * t * t + | AtomicType of t * t array + +let kind_of_type sigma t = match kind sigma t with + | Sort s -> SortType s + | Cast (c,_,t) -> CastType (c, t) + | Prod (na,t,c) -> ProdType (na, t, c) + | LetIn (na,b,t,c) -> LetInType (na, b, t, c) + | App (c,l) -> AtomicType (c, l) + | (Rel _ | Meta _ | Var _ | Evar _ | Const _ + | Proj _ | Case _ | Fix _ | CoFix _ | Ind _) + -> AtomicType (t,[||]) + | (Lambda _ | Construct _ | Int _ | Float _) -> failwith "Not a type" module Unsafe = struct diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 90f50b764c..9a73c3e3f5 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -80,7 +80,14 @@ val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t val to_constr_opt : Evd.evar_map -> t -> Constr.t option (** Same as [to_constr], but returns [None] if some unresolved evars remain *) -val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type +type kind_of_type = + | SortType of ESorts.t + | CastType of types * t + | ProdType of Name.t Context.binder_annot * t * t + | LetInType of Name.t Context.binder_annot * t * t * t + | AtomicType of t * t array + +val kind_of_type : Evd.evar_map -> t -> kind_of_type (** {5 Constructors} *) @@ -152,6 +159,7 @@ val mkNamedProd_or_LetIn : named_declaration -> types -> types val isRel : Evd.evar_map -> t -> bool val isVar : Evd.evar_map -> t -> bool val isInd : Evd.evar_map -> t -> bool +val isRef : Evd.evar_map -> t -> bool val isEvar : Evd.evar_map -> t -> bool val isMeta : Evd.evar_map -> t -> bool val isSort : Evd.evar_map -> t -> bool @@ -175,6 +183,7 @@ val isArity : Evd.evar_map -> t -> bool val isVarId : Evd.evar_map -> Id.t -> t -> bool val isRelN : Evd.evar_map -> int -> t -> bool +val isRefX : Evd.evar_map -> GlobRef.t -> t -> bool val destRel : Evd.evar_map -> t -> int val destMeta : Evd.evar_map -> t -> metavariable @@ -319,6 +328,7 @@ val fresh_global : Evd.evar_map -> GlobRef.t -> Evd.evar_map * t val is_global : Evd.evar_map -> GlobRef.t -> t -> bool +[@@ocaml.deprecated "Use [EConstr.isRefX] instead."] (** {5 Extra} *) diff --git a/engine/evar_kinds.ml b/engine/evar_kinds.ml index bfe0aa3544..71d68f739e 100644 --- a/engine/evar_kinds.ml +++ b/engine/evar_kinds.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/engine/evar_kinds.mli b/engine/evar_kinds.mli index 008633d754..ffc57cfd15 100644 --- a/engine/evar_kinds.mli +++ b/engine/evar_kinds.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/engine/evarutil.ml b/engine/evarutil.ml index b09cc87f97..fdcdfe11f4 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -555,7 +555,7 @@ let rec check_and_clear_in_constr env evdref err ids global c = let () = if global then let check id' = if Id.Set.mem id' ids then - raise (ClearDependencyError (id',err,Some (Globnames.global_of_constr c))) + raise (ClearDependencyError (id',err,Some (fst @@ destRef c))) in Id.Set.iter check (Environ.vars_of_global env (fst @@ destRef c)) in diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 65a069a280..1dec63aaf0 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/engine/evd.ml b/engine/evd.ml index 94868d9bdd..65fe261ff4 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -200,13 +200,14 @@ let evar_filtered_hyps evi = match Filter.repr (evar_filter evi) with in make_hyps filter (evar_context evi) -let evar_env evi = Global.env_of_context evi.evar_hyps +let evar_env env evi = + Environ.reset_with_named_context evi.evar_hyps env -let evar_filtered_env evi = match Filter.repr (evar_filter evi) with -| None -> evar_env evi +let evar_filtered_env env evi = match Filter.repr (evar_filter evi) with +| None -> evar_env env evi | Some filter -> let rec make_env filter ctxt = match filter, ctxt with - | [], [] -> reset_context (Global.env ()) + | [], [] -> reset_context env | false :: filter, _ :: ctxt -> make_env filter ctxt | true :: filter, decl :: ctxt -> let env = make_env filter ctxt in @@ -901,14 +902,14 @@ let make_nonalgebraic_variable evd u = let fresh_sort_in_family ?loc ?(rigid=univ_flexible) evd s = with_context_set ?loc rigid evd (UnivGen.fresh_sort_in_family s) -let fresh_constant_instance ?loc env evd c = - with_context_set ?loc univ_flexible evd (UnivGen.fresh_constant_instance env c) +let fresh_constant_instance ?loc ?(rigid=univ_flexible) env evd c = + with_context_set ?loc rigid evd (UnivGen.fresh_constant_instance env c) -let fresh_inductive_instance ?loc env evd i = - with_context_set ?loc univ_flexible evd (UnivGen.fresh_inductive_instance env i) +let fresh_inductive_instance ?loc ?(rigid=univ_flexible) env evd i = + with_context_set ?loc rigid evd (UnivGen.fresh_inductive_instance env i) -let fresh_constructor_instance ?loc env evd c = - with_context_set ?loc univ_flexible evd (UnivGen.fresh_constructor_instance env c) +let fresh_constructor_instance ?loc ?(rigid=univ_flexible) env evd c = + with_context_set ?loc rigid evd (UnivGen.fresh_constructor_instance env c) let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr = with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?loc ?names env gr) @@ -1363,7 +1364,6 @@ module MiniEConstr = struct let kind sigma c = Constr.kind (whd_evar sigma c) let kind_upto = kind - let kind_of_type sigma c = Term.kind_of_type (whd_evar sigma c) let of_kind = Constr.of_kind let of_constr c = c let of_constr_array v = v diff --git a/engine/evd.mli b/engine/evd.mli index 7876e9a48f..bbdb63a467 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -125,8 +125,8 @@ val evar_filtered_hyps : evar_info -> named_context_val val evar_body : evar_info -> evar_body val evar_candidates : evar_info -> constr list option val evar_filter : evar_info -> Filter.t -val evar_env : evar_info -> env -val evar_filtered_env : evar_info -> env +val evar_env : env -> evar_info -> env +val evar_filtered_env : env -> evar_info -> env val map_evar_body : (econstr -> econstr) -> evar_body -> evar_body val map_evar_info : (econstr -> econstr) -> evar_info -> evar_info @@ -653,10 +653,14 @@ val update_sigma_env : evar_map -> env -> evar_map (** Polymorphic universes *) -val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> evar_map -> Sorts.family -> evar_map * Sorts.t -val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> Constant.t -> evar_map * pconstant -val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive -val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor +val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid + -> evar_map -> Sorts.family -> evar_map * Sorts.t +val fresh_constant_instance : ?loc:Loc.t -> ?rigid:rigid + -> env -> evar_map -> Constant.t -> evar_map * pconstant +val fresh_inductive_instance : ?loc:Loc.t -> ?rigid:rigid + -> env -> evar_map -> inductive -> evar_map * pinductive +val fresh_constructor_instance : ?loc:Loc.t -> ?rigid:rigid + -> env -> evar_map -> constructor -> evar_map * pconstructor val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> GlobRef.t -> evar_map * econstr @@ -707,7 +711,6 @@ module MiniEConstr : sig val kind : evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term val kind_upto : evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term - val kind_of_type : evar_map -> t -> (t, t) Term.kind_of_type val whd_evar : evar_map -> t -> t diff --git a/engine/ftactic.ml b/engine/ftactic.ml index a727375c8d..70488fb4e8 100644 --- a/engine/ftactic.ml +++ b/engine/ftactic.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/engine/ftactic.mli b/engine/ftactic.mli index 666a74d283..731a4ad4ec 100644 --- a/engine/ftactic.mli +++ b/engine/ftactic.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index 3c383b2e00..4c7ed9047d 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -38,9 +38,9 @@ exception Tac_Timeout exception TacticFailure of exn let _ = CErrors.register_handler begin function - | Exception e -> CErrors.print e - | TacticFailure e -> CErrors.print e - | _ -> raise CErrors.Unhandled + | Exception e -> Some (CErrors.print e) + | TacticFailure e -> Some (CErrors.print e) + | _ -> None end (** {6 Non-logical layer} *) @@ -83,17 +83,18 @@ struct (** [Pervasives.raise]. Except that exceptions are wrapped with {!Exception}. *) - let raise ?info = fun e -> (); fun () -> Exninfo.raise ?info (Exception e) + let raise (e, info) () = Exninfo.iraise (Exception e, info) (** [try ... with ...] but restricted to {!Exception}. *) let catch = fun s h -> (); fun () -> try s () with Exception e as src -> - let (src, info) = CErrors.push src in + let (src, info) = Exninfo.capture src in h (e, info) () let read_line = fun () -> try read_line () with e -> - let (e, info) = CErrors.push e in raise ~info e () + let (e, info) = Exninfo.capture e in + raise (e,info) () let print_char = fun c -> (); fun () -> print_char c @@ -103,8 +104,8 @@ struct let make f = (); fun () -> try f () with e when CErrors.noncritical e -> - let (e, info) = CErrors.push e in - Util.iraise (Exception e, info) + let (e, info) = Exninfo.capture e in + Exninfo.iraise (Exception e, info) (** Use the current logger. The buffer is also flushed. *) let print_debug s = make (fun _ -> Feedback.msg_debug s) @@ -114,8 +115,8 @@ struct let run = fun x -> try x () with Exception e as src -> - let (src, info) = CErrors.push src in - Util.iraise (e, info) + let (src, info) = Exninfo.capture src in + Exninfo.iraise (e, info) end (** {6 Logical layer} *) diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli index 75920455ce..7df29c6653 100644 --- a/engine/logic_monad.mli +++ b/engine/logic_monad.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -70,7 +70,7 @@ module NonLogical : sig (** [Pervasives.raise]. Except that exceptions are wrapped with {!Exception}. *) - val raise : ?info:Exninfo.info -> exn -> 'a t + val raise : Exninfo.iexn -> 'a t (** [try ... with ...] but restricted to {!Exception}. *) val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t diff --git a/engine/namegen.ml b/engine/namegen.ml index 56277e8092..370f35f6ed 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -216,7 +216,6 @@ let it_mkLambda_or_LetIn_name env sigma b hyps = let get_mangle_names = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"mangle auto-generated names" ~key:["Mangle";"Names"] ~value:false @@ -227,7 +226,6 @@ let set_prefix x = mangle_names_prefix := forget_subscript x let () = Goptions.( declare_string_option { optdepr = false; - optname = "mangled names prefix"; optkey = ["Mangle";"Names";"Prefix"]; optread = (fun () -> Id.to_string !mangle_names_prefix); optwrite = begin fun x -> @@ -261,15 +259,17 @@ let visible_ids sigma (nenv, c) = let (gseen, vseen, ids) = !accu in let g = global_of_constr c in if not (GlobRef.Set_env.mem g gseen) then - begin - try let gseen = GlobRef.Set_env.add g gseen in - let short = Nametab.shortest_qualid_of_global Id.Set.empty g in - let dir, id = repr_qualid short in - let ids = if DirPath.is_empty dir then Id.Set.add id ids else ids in + let ids = match Nametab.shortest_qualid_of_global Id.Set.empty g with + | short -> + let dir, id = repr_qualid short in + if DirPath.is_empty dir then Id.Set.add id ids else ids + | exception Not_found -> + (* This may happen if given pathological terms or when manipulating + open modules *) + ids + in accu := (gseen, vseen, ids) - with Not_found when !Flags.in_debugger || !Flags.in_toplevel -> () - end | Rel p -> let (gseen, vseen, ids) = !accu in if p > n && not (Int.Set.mem p vseen) then diff --git a/engine/namegen.mli b/engine/namegen.mli index 4a1cd4d44f..b8c5f3202e 100644 --- a/engine/namegen.mli +++ b/engine/namegen.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/engine/nameops.ml b/engine/nameops.ml index fe0a91e3ba..b617865c0d 100644 --- a/engine/nameops.ml +++ b/engine/nameops.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/engine/nameops.mli b/engine/nameops.mli index a0f3a72233..3f7714b3e0 100644 --- a/engine/nameops.mli +++ b/engine/nameops.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/engine/proofview.ml b/engine/proofview.ml index 6f8e668e4e..2e036be9e3 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -228,7 +228,7 @@ let apply ~name ~poly env t sp = let ans = Proof.repr (Proof.run t P.{trace=false; name; poly} (sp,env)) in let ans = Logic_monad.NonLogical.run ans in match ans with - | Nil (e, info) -> iraise (TacticFailure e, info) + | Nil (e, info) -> Exninfo.iraise (TacticFailure e, info) | Cons ((r, (state, _), status, info), _) -> let (status, gaveup) = status in let status = (status, state.shelf, gaveup) in @@ -262,6 +262,8 @@ module Monad = Proof (** [tclZERO e] fails with exception [e]. It has no success. *) let tclZERO ?info e = + if not (CErrors.noncritical e) then + CErrors.anomaly (Pp.str "tclZERO receiving critical error: " ++ CErrors.print e); let info = match info with | None -> Exninfo.null | Some info -> info @@ -302,8 +304,9 @@ let tclONCE = Proof.once exception MoreThanOneSuccess let _ = CErrors.register_handler begin function - | MoreThanOneSuccess -> CErrors.user_err Pp.(str "This tactic has more than one success.") - | _ -> raise CErrors.Unhandled + | MoreThanOneSuccess -> + Some (Pp.str "This tactic has more than one success.") + | _ -> None end (** [tclEXACTLY_ONCE e t] succeeds as [t] if [t] has exactly one @@ -327,8 +330,8 @@ let tclEXACTLY_ONCE e t = (** [tclCASE t] wraps the {!Proofview_monad.Logical.split} primitive. *) type 'a case = -| Fail of iexn -| Next of 'a * (iexn -> 'a tactic) +| Fail of Exninfo.iexn +| Next of 'a * (Exninfo.iexn -> 'a tactic) let tclCASE t = let open Logic_monad in let map = function @@ -347,9 +350,8 @@ exception NoSuchGoals of int let _ = CErrors.register_handler begin function | NoSuchGoals n -> - CErrors.user_err - (str "No such " ++ str (String.plural n "goal") ++ str ".") - | _ -> raise CErrors.Unhandled + Some (str "No such " ++ str (String.plural n "goal") ++ str ".") + | _ -> None end (** [tclFOCUS ?nosuchgoal i j t] applies [t] in a context where @@ -420,13 +422,11 @@ let tclFOCUSID ?(nosuchgoal=tclZERO (NoSuchGoals 1)) id t = exception SizeMismatch of int*int let _ = CErrors.register_handler begin function | SizeMismatch (i,j) -> - let open Pp in - let errmsg = - str"Incorrect number of goals" ++ spc() ++ - str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")." - in - CErrors.user_err errmsg - | _ -> raise CErrors.Unhandled + let open Pp in + Some ( + str"Incorrect number of goals" ++ spc() ++ + str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str").") + | _ -> None end (** A variant of [Monad.List.iter] where we iter over the focused list @@ -910,8 +910,9 @@ let tclPROGRESS t = tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS", Pp.str "Failed to progress.")) let _ = CErrors.register_handler begin function - | Logic_monad.Tac_Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") - | _ -> raise CErrors.Unhandled + | Logic_monad.Tac_Timeout -> + Some (Pp.str "[Proofview.tclTIMEOUT] Tactic timeout!") + | _ -> None end let tclTIMEOUT n t = @@ -939,7 +940,7 @@ let tclTIMEOUT n t = return (Util.Inr (Logic_monad.Tac_Timeout, info)) | Logic_monad.TacticFailure e -> return (Util.Inr (e, info)) - | e -> Logic_monad.NonLogical.raise ~info e + | e -> Logic_monad.NonLogical.raise (e, info) end end >>= function | Util.Inl (res,s,m,i) -> @@ -1039,9 +1040,9 @@ let (>>=) = tclBIND (** {6 Goal-dependent tactics} *) -let goal_env evars gl = +let goal_env env evars gl = let evi = Evd.find evars gl in - Evd.evar_filtered_env evi + Evd.evar_filtered_env env evi let goal_nf_evar sigma gl = let evi = Evd.find sigma gl in @@ -1097,7 +1098,7 @@ module Goal = struct let (gl, sigma) = nf_gmake env sigma goal in tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f gl)) with e when catchable_exception e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in tclZERO ~info e end end @@ -1115,7 +1116,7 @@ module Goal = struct tclEVARMAP >>= fun sigma -> try f (gmake env sigma goal) with e when catchable_exception e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in tclZERO ~info e end end @@ -1128,7 +1129,7 @@ module Goal = struct tclEVARMAP >>= fun sigma -> try f (gmake env sigma goal) with e when catchable_exception e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in tclZERO ~info e end | _ -> @@ -1219,7 +1220,7 @@ module V82 = struct InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"<unknown>")) >> Pv.set { ps with solution = evd; comb = sgs; } with e when catchable_exception e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in tclZERO ~info e @@ -1256,13 +1257,14 @@ module V82 = struct let of_tactic t gls = try + let env = Global.env () in let init = { shelf = []; solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in let name, poly = Names.Id.of_string "legacy_pe", false in - let (_,final,_,_) = apply ~name ~poly (goal_env gls.Evd.sigma gls.Evd.it) t init in + let (_,final,_,_) = apply ~name ~poly (goal_env env gls.Evd.sigma gls.Evd.it) t init in { Evd.sigma = final.solution ; it = CList.map drop_state final.comb } with Logic_monad.TacticFailure e as src -> - let (_, info) = CErrors.push src in - iraise (e, info) + let (_, info) = Exninfo.capture src in + Exninfo.iraise (e, info) let put_status = Status.put @@ -1271,7 +1273,7 @@ module V82 = struct let wrap_exceptions f = try f () with e when catchable_exception e -> - let (e, info) = CErrors.push e in tclZERO ~info e + let (e, info) = Exninfo.capture e in tclZERO ~info e end diff --git a/engine/proofview.mli b/engine/proofview.mli index a92179ab5b..d0a2b37a69 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -14,7 +14,6 @@ ['a tactic] is the (abstract) type of tactics modifying the proof state and returning a value of type ['a]. *) -open Util open EConstr (** Main state of tactics *) @@ -187,25 +186,27 @@ module Monad : Monad.S with type +'a t = 'a tactic (** {7 Failure and backtracking} *) -(** [tclZERO e] fails with exception [e]. It has no success. *) +(** [tclZERO e] fails with exception [e]. It has no success. + Exception is supposed to be non critical *) val tclZERO : ?info:Exninfo.info -> exn -> 'a tactic (** [tclOR t1 t2] behaves like [t1] as long as [t1] succeeds. Whenever the successes of [t1] have been depleted and it failed with [e], then it behaves as [t2 e]. In other words, [tclOR] inserts a - backtracking point. *) -val tclOR : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic + backtracking point. In [t2], exception can be assumed non critical. *) +val tclOR : 'a tactic -> (Exninfo.iexn -> 'a tactic) -> 'a tactic (** [tclORELSE t1 t2] is equal to [t1] if [t1] has at least one success or [t2 e] if [t1] fails with [e]. It is analogous to [try/with] handler of exception in that it is not a backtracking - point. *) -val tclORELSE : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic + point. In [t2], exception can be assumed non critical. *) +val tclORELSE : 'a tactic -> (Exninfo.iexn -> 'a tactic) -> 'a tactic (** [tclIFCATCH a s f] is a generalisation of {!tclORELSE}: if [a] succeeds at least once then it behaves as [tclBIND a s] otherwise, - if [a] fails with [e], then it behaves as [f e]. *) -val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (iexn -> 'b tactic) -> 'b tactic + if [a] fails with [e], then it behaves as [f e]. In [f] + exception can be assumed non critical. *) +val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (Exninfo.iexn -> 'b tactic) -> 'b tactic (** [tclONCE t] behave like [t] except it has at most one success: [tclONCE t] stops after the first success of [t]. If [t] fails @@ -213,8 +214,9 @@ val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (iexn -> 'b tactic) -> 'b tac val tclONCE : 'a tactic -> 'a tactic (** [tclEXACTLY_ONCE e t] succeeds as [t] if [t] has exactly one - success. Otherwise it fails. The tactic [t] is run until its first - success, then a failure with exception [e] is simulated. It [t] + success. Otherwise it fails. The tactic [t] is run until its + first success, then a failure with exception [e] is + simulated ([e] has to be non critical). If [t] yields another success, then [tclEXACTLY_ONCE e t] fails with [MoreThanOneSuccess] (it is a user error). Otherwise, [tclEXACTLY_ONCE e t] succeeds with the first success of @@ -227,8 +229,8 @@ val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic continuation. It is the most general primitive to control backtracking. *) type 'a case = - | Fail of iexn - | Next of 'a * (iexn -> 'a tactic) + | Fail of Exninfo.iexn + | Next of 'a * (Exninfo.iexn -> 'a tactic) val tclCASE : 'a tactic -> 'a case tactic (** [tclBREAK p t] is a generalization of [tclONCE t]. Instead of @@ -236,7 +238,7 @@ val tclCASE : 'a tactic -> 'a case tactic failure with an exception [e] such that [p e = Some e'] is raised. At which point it drops the remaining successes, failing with [e']. [tclONCE t] is equivalent to [tclBREAK (fun e -> Some e) t]. *) -val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic +val tclBREAK : (Exninfo.iexn -> Exninfo.iexn option) -> 'a tactic -> 'a tactic (** {7 Focusing tactics} *) @@ -508,8 +510,8 @@ end module UnsafeRepr : sig type state = Proofview_monad.Logical.Unsafe.state - val repr : 'a tactic -> ('a, state, state, iexn) Logic_monad.BackState.t - val make : ('a, state, state, iexn) Logic_monad.BackState.t -> 'a tactic + val repr : 'a tactic -> ('a, state, state, Exninfo.iexn) Logic_monad.BackState.t + val make : ('a, state, state, Exninfo.iexn) Logic_monad.BackState.t -> 'a tactic end (** {6 Goal-dependent tactics} *) diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml index 37f6b5e352..2f53d5bc73 100644 --- a/engine/proofview_monad.ml +++ b/engine/proofview_monad.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli index 342bfa2806..a32b27904d 100644 --- a/engine/proofview_monad.mli +++ b/engine/proofview_monad.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/engine/termops.ml b/engine/termops.ml index a65b8275e6..16f2a87c1e 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -1066,19 +1066,9 @@ let global_of_constr sigma c = | Var id -> VarRef id, EConstr.EInstance.empty | _ -> raise Not_found -let is_global sigma c t = - let open GlobRef in - match c, EConstr.kind sigma t with - | ConstRef c, Const (c', _) -> Constant.equal c c' - | IndRef i, Ind (i', _) -> eq_ind i i' - | ConstructRef i, Construct (i', _) -> eq_constructor i i' - | VarRef id, Var id' -> Id.equal id id' - | _ -> false +let is_global = EConstr.isRefX -let isGlobalRef sigma c = - match EConstr.kind sigma c with - | Const _ | Ind _ | Construct _ | Var _ -> true - | _ -> false +let isGlobalRef = EConstr.isRef let is_template_polymorphic_ind env sigma f = match EConstr.kind sigma f with diff --git a/engine/termops.mli b/engine/termops.mli index f970b9ece0..4e77aa9b3b 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -264,10 +264,13 @@ val dependency_closure : env -> Evd.evar_map -> named_context -> Id.Set.t -> Id. val is_section_variable : Id.t -> bool val global_of_constr : Evd.evar_map -> constr -> GlobRef.t * EInstance.t +[@@ocaml.deprecated "Use [EConstr.destRef] instead (throws DestKO instead of Not_found)."] val is_global : Evd.evar_map -> GlobRef.t -> constr -> bool +[@@ocaml.deprecated "Use [EConstr.isRefX] instead."] val isGlobalRef : Evd.evar_map -> constr -> bool +[@@ocaml.deprecated "Use [EConstr.isRef] instead."] val is_template_polymorphic_ind : env -> Evd.evar_map -> constr -> bool diff --git a/engine/uState.ml b/engine/uState.ml index 3546ece581..d532129dc5 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -53,7 +53,7 @@ let empty = uctx_weak_constraints = UPairSet.empty; } let elaboration_sprop_cumul = - Goptions.declare_bool_option_and_ref ~depr:false ~name:"SProp cumulativity during elaboration" + Goptions.declare_bool_option_and_ref ~depr:false ~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true let make ~lbound u = diff --git a/engine/uState.mli b/engine/uState.mli index 8855a6bea6..3959373ead 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/engine/univGen.ml b/engine/univGen.ml index 1fe09270ba..6f27ccb7dc 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -48,8 +48,6 @@ let fresh_instance_from ?loc ctx = function (** Fresh universe polymorphic construction *) -open Globnames - let fresh_global_instance ?loc ?names env gr = let auctx = Environ.universes_of_global env gr in let u, ctx = fresh_instance_from ?loc auctx names in @@ -78,10 +76,6 @@ let constr_of_monomorphic_global gr = Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++ str " would forget universes.") -let fresh_global_or_constr_instance env = function - | IsConstr c -> c, ContextSet.empty - | IsGlobal gr -> fresh_global_instance env gr - let fresh_sort_in_family = function | InSProp -> Sorts.sprop, ContextSet.empty | InProp -> Sorts.prop, ContextSet.empty diff --git a/engine/univGen.mli b/engine/univGen.mli index 1b351c61c4..81bdac17ce 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -46,9 +46,6 @@ val fresh_constructor_instance : env -> constructor -> val fresh_global_instance : ?loc:Loc.t -> ?names:Univ.Instance.t -> env -> GlobRef.t -> constr in_universe_context_set -val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> - constr in_universe_context_set - (** Get fresh variables for the universe context. Useful to make tactics that manipulate constrs in universe contexts polymorphic. *) val fresh_universe_context_set_instance : ContextSet.t -> diff --git a/engine/univMinim.ml b/engine/univMinim.ml index fc0770cf75..c05a7a800d 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -15,7 +15,6 @@ open UnivSubst let get_set_minimization = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"minimization to Set" ~key:["Universe";"Minimization";"ToSet"] ~value:true diff --git a/engine/univMinim.mli b/engine/univMinim.mli index 72b432e62f..2a46d87609 100644 --- a/engine/univMinim.mli +++ b/engine/univMinim.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/engine/univNames.ml b/engine/univNames.ml index 887191f9b7..6d9095680c 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/engine/univNames.mli b/engine/univNames.mli index ebb665c4fd..34a18d6b6e 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/engine/univProblem.ml b/engine/univProblem.ml index 07cde25564..08ff9efa5b 100644 --- a/engine/univProblem.ml +++ b/engine/univProblem.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/engine/univProblem.mli b/engine/univProblem.mli index 68c5d4cd5e..575f5ac847 100644 --- a/engine/univProblem.mli +++ b/engine/univProblem.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/engine/univSubst.ml b/engine/univSubst.ml index 737eb83a3d..6000650ad9 100644 --- a/engine/univSubst.ml +++ b/engine/univSubst.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/engine/univSubst.mli b/engine/univSubst.mli index fc10a694e9..293774f0bd 100644 --- a/engine/univSubst.mli +++ b/engine/univSubst.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/engine/univops.ml b/engine/univops.ml index 92f69317fd..2738021964 100644 --- a/engine/univops.ml +++ b/engine/univops.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/engine/univops.mli b/engine/univops.mli index 1f1edbed16..02a731ad49 100644 --- a/engine/univops.mli +++ b/engine/univops.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |