aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_types.ml8
-rw-r--r--plugins/funind/functional_principles_types.mli4
-rw-r--r--plugins/funind/g_indfun.mlg4
-rw-r--r--plugins/funind/gen_principle.ml76
-rw-r--r--plugins/funind/gen_principle.mli4
-rw-r--r--plugins/funind/glob_term_to_relation.ml4
-rw-r--r--plugins/funind/glob_termops.ml4
-rw-r--r--plugins/funind/glob_termops.mli4
-rw-r--r--plugins/funind/indfun.ml4
-rw-r--r--plugins/funind/indfun.mli4
-rw-r--r--plugins/funind/invfun.ml4
-rw-r--r--plugins/funind/invfun.mli4
-rw-r--r--plugins/funind/recdef.ml4
13 files changed, 59 insertions, 69 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 797d421c56..163645b719 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.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 *)
@@ -63,14 +63,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
(* observe (str "princ_infos : " ++ pr_elim_scheme princ_type_info); *)
let change_predicate_sort i decl =
let new_sort = sorts.(i) in
- let args,_ = decompose_prod (EConstr.Unsafe.to_constr (RelDecl.get_type decl)) in
+ let args,_ = decompose_prod_assum (EConstr.Unsafe.to_constr (RelDecl.get_type decl)) in
let real_args =
if princ_type_info.indarg_in_concl
then List.tl args
else args
in
Context.Named.Declaration.LocalAssum (map_annot Nameops.Name.get_id (Context.Rel.Declaration.get_annot decl),
- Term.compose_prod real_args (mkSort new_sort))
+ Term.it_mkProd_or_LetIn (mkSort new_sort) real_args)
in
let new_predicates =
List.map_i
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index 6f060b0146..c870603a43 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.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/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index a02cb24bee..68e1087b74 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -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/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 68661174ac..d38c3c869b 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.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 *)
@@ -39,7 +39,7 @@ let build_newrecursive lnameargsardef =
List.fold_left
(fun (env,impls) { Vernacexpr.fname={CAst.v=recname}; binders; rtype } ->
let arityc = Constrexpr_ops.mkCProdN binders rtype in
- let arity,ctx = Constrintern.interp_type env0 sigma arityc in
+ let arity,_ctx = Constrintern.interp_type env0 sigma arityc in
let evd = Evd.from_env env0 in
let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd binders in
let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in
@@ -164,7 +164,7 @@ let prepare_body { Vernacexpr.binders } rt =
let fun_args,rt' = chop_rlambda_n n rt in
(fun_args,rt')
-let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook =
+let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_map ref) old_princ_type sorts funs _i proof_tac hook =
(* First we get the type of the old graph principle *)
let mutr_nparams = (Tactics.compute_elim_sig !evd (EConstr.of_constr old_princ_type)).Tactics.nparams in
(* let time1 = System.get_time () in *)
@@ -199,7 +199,7 @@ let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_
(* end; *)
let open Proof_global in
- let { name; entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)) lemma in
+ let { entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false) lemma in
match entries with
| [entry] ->
entry, hook
@@ -235,7 +235,6 @@ let change_property_sort evd toSort princ princName =
(List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) princ_info.Tactics.params)
let generate_functional_principle (evd: Evd.evar_map ref)
- interactive_proof
old_princ_type sorts new_princ_name funs i proof_tac
=
try
@@ -283,26 +282,25 @@ let generate_functional_principle (evd: Evd.evar_map ref)
register_with_sort Sorts.InSet
in
let entry, hook =
- build_functional_principle evd interactive_proof old_princ_type new_sorts funs i
+ build_functional_principle evd old_princ_type new_sorts funs i
proof_tac hook
in
(* Pr 1278 :
Don't forget to close the goal if an error is raised !!!!
*)
let uctx = Evd.evar_universe_context sigma in
- let hook_data = hook, uctx, [] in
- let _ : Names.GlobRef.t = DeclareDef.declare_definition
- ~name:new_princ_name ~hook_data
+ let _ : Names.GlobRef.t = DeclareDef.declare_entry
+ ~name:new_princ_name ~hook
~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
~kind:Decls.(IsProof Theorem)
- UnivNames.empty_binders
- entry [] in
+ ~impargs:[]
+ ~uctx entry in
()
with e when CErrors.noncritical e ->
raise (Defining_principle e)
let generate_principle (evd:Evd.evar_map ref) pconstants on_error
- is_general do_built fix_rec_l recdefs interactive_proof
+ is_general do_built fix_rec_l recdefs
(continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int ->
Tacmach.tactic) : unit =
let names = List.map (function { Vernacexpr.fname = {CAst.v=name} } -> name) fix_rec_l in
@@ -335,7 +333,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
let funs_kn = Array.of_list (List.map fname_kn fix_rec_l) in
let _ =
List.map_i
- (fun i x ->
+ (fun i _x ->
let env = Global.env () in
let princ = Indrec.lookup_eliminator env (ind_kn,i) (Sorts.InProp) in
let evd = ref (Evd.from_env env) in
@@ -346,7 +344,6 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
let princ_type = EConstr.Unsafe.to_constr princ_type in
generate_functional_principle
evd
- interactive_proof
princ_type
None
None
@@ -374,7 +371,6 @@ let register_struct is_rec fixpoint_exprl =
| None ->
CErrors.user_err ~hdr:"Function" Pp.(str "Body of Function must be given") in
ComDefinition.do_definition
- ~program_mode:false
~name:fname.CAst.v
~poly:false
~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
@@ -412,7 +408,7 @@ let register_struct is_rec fixpoint_exprl =
None,evd,List.rev rev_pconstants
let generate_correction_proof_wf f_ref tcc_lemma_ref
- is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
+ is_mes functional_ref eq_ref rec_arg_num rec_arg_type relation
(_: int) (_:Names.Constant.t array) (_:EConstr.constr array) (_:int) : Tacmach.tactic =
Functional_principles_proofs.prove_principle_for_gen
(f_ref,functional_ref,eq_ref)
@@ -430,7 +426,7 @@ let generate_correction_proof_wf f_ref tcc_lemma_ref
res = fv \rightarrow graph\ x_1\ldots x_n\ res\] decomposed as the context and the conclusion
*)
-let generate_type evd g_to_f f graph i =
+let generate_type evd g_to_f f graph =
let open Context.Rel.Declaration in
let open EConstr in
let open EConstr.Vars in
@@ -498,7 +494,7 @@ let generate_type evd g_to_f f graph i =
WARNING: while convertible, [type_of body] and [type] can be non equal
*)
let find_induction_principle evd f =
- let f_as_constant,u = match EConstr.kind !evd f with
+ let f_as_constant, _u = match EConstr.kind !evd f with
| Constr.Const c' -> c'
| _ -> CErrors.user_err Pp.(str "Must be used with a function")
in
@@ -545,7 +541,7 @@ let rec generate_fresh_id x avoid i =
let id = Namegen.next_ident_away_in_goal x (Id.Set.of_list avoid) in
id::(generate_fresh_id x (id::avoid) (pred i))
-let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i : Tacmach.tactic =
+let prove_fun_correct evd graphs_constr schemes lemmas_types_infos i : Tacmach.tactic =
let open Constr in
let open EConstr in
let open Context.Rel.Declaration in
@@ -1140,7 +1136,7 @@ let get_funs_constant mp =
to prevent Reset strange thing
*)
let l_bodies = List.map find_constant_body (Array.to_list (Array.map fst l_const)) in
- let l_params,l_fixes = List.split (List.map Term.decompose_lam l_bodies) in
+ let l_params, _l_fixes = List.split (List.map Term.decompose_lam l_bodies) in
(* all the parameters must be equal*)
let _check_params =
let first_params = List.hd l_params in
@@ -1240,7 +1236,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
in
let entry, _hook =
try
- build_functional_principle ~opaque evd false
+ build_functional_principle ~opaque evd
first_type
(Array.of_list sorts)
this_block_funs
@@ -1261,7 +1257,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
let sorts = Array.of_list sorts in
List.map (Functional_principles_types.compute_new_princ_type_from_rel funs sorts) other_princ_types
in
- let first_princ_body,first_princ_type = Declare.(entry.proof_entry_body, entry.proof_entry_type) in
+ let first_princ_body = entry.Declare.proof_entry_body in
let ctxt,fix = Term.decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*)
let (idxs,_),(_,ta,_ as decl) = Constr.destFix fix in
let other_result =
@@ -1291,7 +1287,6 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
let entry, _hook =
build_functional_principle
evd
- false
(List.nth other_princ_types (!i - 1))
(Array.of_list sorts)
this_block_funs
@@ -1330,9 +1325,8 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) =
let lemmas_types_infos =
Util.Array.map2_i
(fun i f_constr graph ->
- (* let const_of_f,u = destConst f_constr in *)
let (type_of_lemma_ctxt,type_of_lemma_concl,graph) =
- generate_type evd false f_constr graph i
+ generate_type evd false f_constr graph
in
let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
graphs_constr.(i) <- graph;
@@ -1367,7 +1361,7 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) =
)
in
let proving_tac =
- prove_fun_correct !evd funs_constr graphs_constr schemes lemmas_types_infos
+ prove_fun_correct !evd graphs_constr schemes lemmas_types_infos
in
Array.iteri
(fun i f_as_constant ->
@@ -1397,8 +1391,8 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) =
let lemmas_types_infos =
Util.Array.map2_i
(fun i f_constr graph ->
- let (type_of_lemma_ctxt,type_of_lemma_concl,graph) =
- generate_type evd true f_constr graph i
+ let (type_of_lemma_ctxt,type_of_lemma_concl,graph) =
+ generate_type evd true f_constr graph
in
let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
graphs_constr.(i) <- graph;
@@ -1414,7 +1408,7 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) =
in
let (kn,_) as graph_ind,u = (destInd !evd graphs_constr.(0)) in
- let mib,mip = Global.lookup_inductive graph_ind in
+ let mib, _mip = Global.lookup_inductive graph_ind in
let sigma, scheme =
(Indrec.build_mutual_induction_scheme (Global.env ()) !evd
(Array.to_list
@@ -1484,7 +1478,7 @@ let derive_inversion fix_names =
*)
List.iter (fun c -> ignore (find_Function_infos (fst c))) fix_names_as_constant ;
try
- let evd', lind =
+ let _evd', lind =
List.fold_right
(fun id (evd,l) ->
let evd,id =
@@ -1535,11 +1529,11 @@ let register_wf interactive_proof ?(is_mes=false) fname rec_impls wf_rel_expr wf
in
let eq = Constrexpr_ops.mkCProdN args unbounded_eq in
let hook ((f_ref,_) as fconst) tcc_lemma_ref (functional_ref,_) (eq_ref,_) rec_arg_num rec_arg_type
- nb_args relation =
+ _nb_args relation =
try
pre_hook [fconst]
(generate_correction_proof_wf f_ref tcc_lemma_ref is_mes
- functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
+ functional_ref eq_ref rec_arg_num rec_arg_type relation
);
derive_inversion [fname]
with e when CErrors.noncritical e ->
@@ -1561,7 +1555,7 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt w
| None ->
begin
match args with
- | [Constrexpr.CLocalAssum ([{CAst.v=Name x}],k,t)] -> t,x
+ | [Constrexpr.CLocalAssum ([{CAst.v=Name x}],_k,t)] -> t,x
| _ -> CErrors.user_err (Pp.str "Recursive argument must be specified")
end
| Some wf_args ->
@@ -1569,7 +1563,7 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt w
match
List.find
(function
- | Constrexpr.CLocalAssum(l,k,t) ->
+ | Constrexpr.CLocalAssum(l,_k,t) ->
List.exists
(function {CAst.v=Name id} -> Id.equal id wf_args | _ -> false)
l
@@ -1577,7 +1571,7 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt w
)
args
with
- | Constrexpr.CLocalAssum(_,k,t) -> t,wf_args
+ | Constrexpr.CLocalAssum(_,_k,t) -> t,wf_args
| _ -> assert false
with Not_found -> assert false
in
@@ -1625,7 +1619,7 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro
let lemma, _is_struct =
match fixpoint_exprl with
| [{ Vernacexpr.rec_order = Some {CAst.v = Constrexpr.CWfRec (wf_x,wf_rel)} } as fixpoint_expr] ->
- let { Vernacexpr.fname; univs; binders; rtype; body_def } as fixpoint_expr =
+ let { Vernacexpr.fname; univs = _; binders; rtype; body_def } as fixpoint_expr =
match recompute_binder_list [fixpoint_expr] with
| [e] -> e
| _ -> assert false
@@ -1644,13 +1638,12 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro
register_built
fixpoint_exprl
recdefs
- true
in
if register_built
then register_wf interactive_proof fname.CAst.v rec_impls wf_rel wf_x.CAst.v using_lemmas binders rtype body pre_hook, false
else None, false
| [{ Vernacexpr.rec_order = Some {CAst.v = Constrexpr.CMeasureRec(wf_x,wf_mes,wf_rel_opt)} } as fixpoint_expr] ->
- let { Vernacexpr.fname; univs; binders; rtype; body_def} as fixpoint_expr =
+ let { Vernacexpr.fname; univs = _; binders; rtype; body_def} as fixpoint_expr =
match recompute_binder_list [fixpoint_expr] with
| [e] -> e
| _ -> assert false
@@ -1671,7 +1664,6 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro
register_built
fixpoint_exprl
recdefs
- true
in
if register_built
then register_mes interactive_proof fname.CAst.v rec_impls wf_mes wf_rel_opt
@@ -1689,7 +1681,7 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro
let fixpoint_exprl = recompute_binder_list fixpoint_exprl in
let fix_names = List.map (function { Vernacexpr.fname } -> fname.CAst.v) fixpoint_exprl in
(* ok all the expressions are structural *)
- let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
+ let recdefs, _rec_impls = build_newrecursive fixpoint_exprl in
let is_rec = List.exists (is_rec fix_names) recdefs in
let lemma,evd,pconstants =
if register_built
@@ -1705,7 +1697,6 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro
register_built
fixpoint_exprl
recdefs
- interactive_proof
(Functional_principles_proofs.prove_princ_for_struct evd interactive_proof);
if register_built then
begin derive_inversion fix_names; end;
@@ -2066,7 +2057,6 @@ let build_case_scheme fa =
*)
generate_functional_principle
(ref (Evd.from_env (Global.env ())))
- false
scheme_type
(Some ([|sorts|]))
(Some princ_name)
diff --git a/plugins/funind/gen_principle.mli b/plugins/funind/gen_principle.mli
index 7eb8ca3af1..6313a2b16e 100644
--- a/plugins/funind/gen_principle.mli
+++ b/plugins/funind/gen_principle.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/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index c7dfe69fb1..e08ad9af3a 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1517,7 +1517,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Vernacexpr.Inductive_kw,repacked_rel_inds)})
+ Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(Vernacexpr.Inductive_kw,repacked_rel_inds)})
++ fnl () ++
msg
in
@@ -1532,7 +1532,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Vernacexpr.Inductive_kw,repacked_rel_inds)})
+ Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(Vernacexpr.Inductive_kw,repacked_rel_inds)})
++ fnl () ++
CErrors.print reraise
in
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index f2d98a13ab..9fa72919ce 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_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 *)
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index bdde66bbd7..c55fdc017c 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_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 *)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index f28e98dcc2..1f2f56ec34 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.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/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 476d74b3f8..4f3d4a1587 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.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/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 332d058ce7..44d2cb4a3d 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.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/plugins/funind/invfun.mli b/plugins/funind/invfun.mli
index 6b789e1bb2..41dbe1437c 100644
--- a/plugins/funind/invfun.mli
+++ b/plugins/funind/invfun.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/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 9fa0ec8c08..19a762d33d 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.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 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 07:26:24 +0000