diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 2 | ||||
| -rw-r--r-- | proofs/clenv.mli | 2 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 4 | ||||
| -rw-r--r-- | proofs/clenvtac.mli | 2 | ||||
| -rw-r--r-- | proofs/evar_refiner.ml | 2 | ||||
| -rw-r--r-- | proofs/evar_refiner.mli | 2 | ||||
| -rw-r--r-- | proofs/goal.ml | 2 | ||||
| -rw-r--r-- | proofs/goal.mli | 2 | ||||
| -rw-r--r-- | proofs/goal_select.ml | 2 | ||||
| -rw-r--r-- | proofs/goal_select.mli | 2 | ||||
| -rw-r--r-- | proofs/logic.ml | 2 | ||||
| -rw-r--r-- | proofs/logic.mli | 2 | ||||
| -rw-r--r-- | proofs/miscprint.ml | 2 | ||||
| -rw-r--r-- | proofs/miscprint.mli | 2 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 33 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 4 | ||||
| -rw-r--r-- | proofs/proof.ml | 2 | ||||
| -rw-r--r-- | proofs/proof.mli | 2 | ||||
| -rw-r--r-- | proofs/proof_bullet.ml | 2 | ||||
| -rw-r--r-- | proofs/proof_bullet.mli | 2 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 173 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 79 | ||||
| -rw-r--r-- | proofs/refine.ml | 7 | ||||
| -rw-r--r-- | proofs/refine.mli | 7 | ||||
| -rw-r--r-- | proofs/refiner.ml | 57 | ||||
| -rw-r--r-- | proofs/refiner.mli | 31 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 11 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 6 | ||||
| -rw-r--r-- | proofs/tactypes.ml | 2 |
29 files changed, 133 insertions, 315 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 2d2113b636..0dcc55a1cb 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.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/proofs/clenv.mli b/proofs/clenv.mli index 03acb9e46e..eecd318287 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.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/proofs/clenvtac.ml b/proofs/clenvtac.ml index c36b0fa337..1904d9b112 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.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 *) @@ -19,7 +19,7 @@ open Reduction open Clenv (* This function put casts around metavariables whose type could not be - * infered by the refiner, that is head of applications, predicates and + * inferred by the refiner, that is head of applications, predicates and * subject of Cases. * Does check that the casted type is closed. Anyway, the refiner would * fail in this case... *) diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index d178478425..2357a1fe30 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.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/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 1a34105ab6..6c9c95e342 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.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/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index e8f3c4d173..8f3ac7ed25 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.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/proofs/goal.ml b/proofs/goal.ml index 94707accab..888c4785df 100644 --- a/proofs/goal.ml +++ b/proofs/goal.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/proofs/goal.mli b/proofs/goal.mli index 665b0c9e59..46b54f9c2c 100644 --- a/proofs/goal.mli +++ b/proofs/goal.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/proofs/goal_select.ml b/proofs/goal_select.ml index 955d797227..a6e27c238f 100644 --- a/proofs/goal_select.ml +++ b/proofs/goal_select.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/proofs/goal_select.mli b/proofs/goal_select.mli index b1c5723885..c322ace9f3 100644 --- a/proofs/goal_select.mli +++ b/proofs/goal_select.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/proofs/logic.ml b/proofs/logic.ml index b79e1e6024..a9843e080e 100644 --- a/proofs/logic.ml +++ b/proofs/logic.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/proofs/logic.mli b/proofs/logic.mli index 406fe57985..1046fd8b29 100644 --- a/proofs/logic.mli +++ b/proofs/logic.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/proofs/miscprint.ml b/proofs/miscprint.ml index ec17b8076f..1092e290c7 100644 --- a/proofs/miscprint.ml +++ b/proofs/miscprint.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/proofs/miscprint.mli b/proofs/miscprint.mli index f4e2e683d1..70a3726605 100644 --- a/proofs/miscprint.mli +++ b/proofs/miscprint.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/proofs/pfedit.ml b/proofs/pfedit.ml index 52e15f466f..e8164a14a7 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.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 *) @@ -42,11 +42,11 @@ let get_goal_context_gen pf i = (sigma, Refiner.pf_env { it=goal ; sigma=sigma; }) let get_goal_context pf i = - let p = Proof_global.give_me_the_proof pf in + let p = Proof_global.get_proof pf in get_goal_context_gen p i let get_current_goal_context pf = - let p = Proof_global.give_me_the_proof pf in + let p = Proof_global.get_proof pf in try get_goal_context_gen p 1 with | NoSuchGoal -> @@ -57,7 +57,7 @@ let get_current_goal_context pf = Evd.from_env env, env let get_current_context pf = - let p = Proof_global.give_me_the_proof pf in + let p = Proof_global.get_proof pf in try get_goal_context_gen p 1 with | NoSuchGoal -> @@ -108,7 +108,7 @@ let solve ?with_end_tac gi info_lvl tac pr = in (p,status) -let by tac = Proof_global.with_current_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac) +let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None tac) (**********************************************************************) (* Shortcut to build a term using tactics *) @@ -117,15 +117,14 @@ open Decl_kinds let next = let n = ref 0 in fun () -> incr n; !n -let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac = +let build_constant_by_tactic id ctx sign ?(goal_kind = Global ImportDefaultBehavior, false, Proof Theorem) typ tac = let evd = Evd.from_ctx ctx in - let terminator = Proof_global.make_terminator (fun _ -> ()) in let goals = [ (Global.env_of_context sign , typ) ] in - let pf = Proof_global.start_proof ~ontop:None evd id goal_kind goals terminator in + let pf = Proof_global.start_proof evd id goal_kind goals in try let pf, status = by tac pf in let open Proof_global in - let { entries; universes } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in + let { entries; universes } = close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in match entries with | [entry] -> let univs = UState.demote_seff_univs entry universes in @@ -139,15 +138,14 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = let id = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in - let gk = Global, poly, Proof Theorem in + let gk = Global ImportDefaultBehavior, poly, Proof Theorem in let ce, status, univs = build_constant_by_tactic id sigma sign ~goal_kind:gk typ tac in - let ce = - if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce - else { ce with - const_entry_body = Future.chain ce.const_entry_body - (fun (pt, _) -> pt, ()) } in - let (cb, ctx), () = Future.force ce.const_entry_body in + let body, eff = Future.force ce.const_entry_body in + let (cb, ctx) = + if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) + else body + in let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in cb, status, univs @@ -197,5 +195,6 @@ let refine_by_tactic ~name ~poly env sigma ty tac = other goals that were already present during its invocation, so that those goals rely on effects that are not present anymore. Hopefully, this hack will work in most cases. *) - let ans = Safe_typing.inline_private_constants_in_constr env ans neff in + let neff = neff.Evd.seff_private in + let (ans, _) = Safe_typing.inline_private_constants env ((ans, Univ.ContextSet.empty), neff) in ans, sigma diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 77d701b41f..2d3b66ff9f 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.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 *) @@ -61,7 +61,7 @@ val use_unification_heuristics : unit -> bool val build_constant_by_tactic : Id.t -> UState.t -> named_context_val -> ?goal_kind:goal_kind -> EConstr.types -> unit Proofview.tactic -> - Safe_typing.private_constants Entries.definition_entry * bool * + Evd.side_effects Entries.definition_entry * bool * UState.t val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:polymorphic -> diff --git a/proofs/proof.ml b/proofs/proof.ml index 09e4e898fe..47502fe402 100644 --- a/proofs/proof.ml +++ b/proofs/proof.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/proofs/proof.mli b/proofs/proof.mli index 248b9d921e..6ef34eed80 100644 --- a/proofs/proof.mli +++ b/proofs/proof.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/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index 640feb2f5b..5702156b65 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.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/proofs/proof_bullet.mli b/proofs/proof_bullet.mli index 6fdf818497..ef4530a363 100644 --- a/proofs/proof_bullet.mli +++ b/proofs/proof_bullet.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/proofs/proof_global.ml b/proofs/proof_global.ml index 40ae4acc88..bddea41145 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.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 *) @@ -29,57 +29,31 @@ type lemma_possible_guards = int list list type proof_object = { id : Names.Id.t; - entries : Safe_typing.private_constants Entries.definition_entry list; + entries : Evd.side_effects Entries.definition_entry list; persistence : Decl_kinds.goal_kind; universes: UState.t; } type opacity_flag = Opaque | Transparent -type proof_ending = - | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t - | Proved of opacity_flag * - lident option * - proof_object - -type proof_terminator = proof_ending -> unit -type closed_proof = proof_object * proof_terminator - -type pstate = { - terminator : proof_terminator CEphemeron.key; - endline_tactic : Genarg.glob_generic_argument option; - section_vars : Constr.named_context option; - proof : Proof.t; - universe_decl: UState.universe_decl; - strength : Decl_kinds.goal_kind; -} - -(* The head of [t] is the actual current proof, the other ones are - to be resumed when the current proof is closed or aborted. *) -type t = pstate * pstate list - -let pstate_map f (pf, pfl) = (f pf, List.map f pfl) - -let make_terminator f = f -let apply_terminator f = f - -(* combinators for the current_proof lists *) -let push ~ontop a = - match ontop with - | None -> a , [] - | Some (l,ls) -> a, (l :: ls) +type t = + { endline_tactic : Genarg.glob_generic_argument option + ; section_vars : Constr.named_context option + ; proof : Proof.t + ; universe_decl: UState.universe_decl + ; strength : Decl_kinds.goal_kind + } (*** Proof Global manipulation ***) -let get_all_proof_names (pf : t) = - let (pn, pns) = pstate_map Proof.(function pf -> (data pf.proof).name) pf in - pn :: pns +let get_proof ps = ps.proof +let get_proof_name ps = (Proof.data ps.proof).Proof.name +let get_persistence ps = ps.strength -let give_me_the_proof (ps,_) = ps.proof -let get_current_proof_name (ps,_) = (Proof.data ps.proof).Proof.name -let get_current_persistence (ps,_) = ps.strength +let map_proof f p = { p with proof = f p.proof } +let map_fold_proof f p = let proof, res = f p.proof in { p with proof }, res -let with_current_proof f (ps, psl) = +let map_fold_proof_endline f ps = let et = match ps.endline_tactic with | None -> Proofview.tclUNIT () @@ -92,30 +66,15 @@ let with_current_proof f (ps, psl) = in let (newpr,ret) = f et ps.proof in let ps = { ps with proof = newpr } in - (ps, psl), ret + ps, ret -let simple_with_current_proof f pf = - let p, () = with_current_proof (fun t p -> f t p , ()) pf in p - -let compact_the_proof pf = simple_with_current_proof (fun _ -> Proof.compact) pf +let compact_the_proof pf = map_proof Proof.compact pf (* Sets the tactic to be used when a tactic line is closed with [...] *) -let set_endline_tactic tac (ps, psl) = - { ps with endline_tactic = Some tac }, psl - -let pf_name_eq id ps = - let Proof.{ name } = Proof.data ps.proof in - Id.equal name id +let set_endline_tactic tac ps = + { ps with endline_tactic = Some tac } -let discard {CAst.loc;v=id} (ps, psl) = - match List.filter (fun pf -> not (pf_name_eq id pf)) (ps :: psl) with - | [] -> None - | ps :: psl -> Some (ps, psl) - -let discard_current (ps, psl) = - if List.is_empty psl then None else Some List.(hd psl, tl psl) - -(** [start_proof sigma id pl str goals terminator] starts a proof of name +(** [start_proof sigma id pl str goals] starts a proof of name [id] with goals [goals] (a list of pairs of environment and conclusion); [str] describes what kind of theorem/definition this is (spiwack: for potential printing, I believe is used only by @@ -123,30 +82,26 @@ let discard_current (ps, psl) = end of the proof to close the proof. The proof is started in the evar map [sigma] (which can typically contain universe constraints), and with universe bindings pl. *) -let start_proof ~ontop sigma name ?(pl=UState.default_univ_decl) kind goals terminator = - let initial_state = { - terminator = CEphemeron.create terminator; - proof = Proof.start ~name ~poly:(pi2 kind) sigma goals; - endline_tactic = None; - section_vars = None; - universe_decl = pl; - strength = kind } in - push ~ontop initial_state - -let start_dependent_proof ~ontop name ?(pl=UState.default_univ_decl) kind goals terminator = - let initial_state = { - terminator = CEphemeron.create terminator; - proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals; - endline_tactic = None; - section_vars = None; - universe_decl = pl; - strength = kind } in - push ~ontop initial_state - -let get_used_variables (pf,_) = pf.section_vars -let get_universe_decl (pf,_) = pf.universe_decl - -let set_used_variables (ps,psl) l = +let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals = + { proof = Proof.start ~name ~poly:(pi2 kind) sigma goals + ; endline_tactic = None + ; section_vars = None + ; universe_decl = pl + ; strength = kind + } + +let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals = + { proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals + ; endline_tactic = None + ; section_vars = None + ; universe_decl = pl + ; strength = kind + } + +let get_used_variables pf = pf.section_vars +let get_universe_decl pf = pf.universe_decl + +let set_used_variables ps l = let open Context.Named.Declaration in let env = Global.env () in let ids = List.fold_right Id.Set.add l Id.Set.empty in @@ -170,16 +125,16 @@ let set_used_variables (ps,psl) l = if not (Option.is_empty ps.section_vars) then CErrors.user_err Pp.(str "Used section variables can be declared only once"); (* EJGA: This is always empty thus we should modify the type *) - (ctx, []), ({ ps with section_vars = Some ctx}, psl) + (ctx, []), { ps with section_vars = Some ctx} -let get_open_goals (ps, _) = +let get_open_goals ps = let Proof.{ goals; stack; shelf } = Proof.data ps.proof in List.length goals + List.fold_left (+) 0 (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) + List.length shelf -type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t +type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t let private_poly_univs = let b = ref true in @@ -195,7 +150,7 @@ let private_poly_univs = let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now (fpl : closed_proof_output Future.computation) ps = - let { section_vars; proof; terminator; universe_decl; strength } = ps in + let { section_vars; proof; universe_decl; strength } = ps in let Proof.{ name; poly; entry; initial_euctx } = Proof.data proof in let opaque = match opaque with Opaque -> true | Transparent -> false in let constrain_variables ctx = @@ -217,7 +172,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now let body = c in let allow_deferred = not poly && (keep_body_ucst_separate || - not (Safe_typing.empty_private_constants = eff)) + not (Safe_typing.empty_private_constants = eff.Evd.seff_private)) in let typ = if allow_deferred then t else nf t in let used_univs_body = Vars.universes_of_constr body in @@ -290,10 +245,9 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now in let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in { id = name; entries = entries; persistence = strength; - universes }, - fun pr_ending -> CEphemeron.get terminator pr_ending + universes } -let return_proof ?(allow_partial=false) (ps,_) = +let return_proof ?(allow_partial=false) ps = let { proof } = ps in if allow_partial then begin let proofs = Proof.partial_proof proof in @@ -322,29 +276,16 @@ let return_proof ?(allow_partial=false) (ps,_) = List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in proofs, Evd.evar_universe_context evd -let close_future_proof ~opaque ~feedback_id (ps, psl) proof = +let close_future_proof ~opaque ~feedback_id ps proof = close_proof ~opaque ~keep_body_ucst_separate:true ~feedback_id ~now:false proof ps -let close_proof ~opaque ~keep_body_ucst_separate fix_exn (ps, psl) = +let close_proof ~opaque ~keep_body_ucst_separate fix_exn ps = close_proof ~opaque ~keep_body_ucst_separate ~now:true - (Future.from_val ~fix_exn (return_proof (ps,psl))) ps - -(** Gets the current terminator without checking that the proof has - been completed. Useful for the likes of [Admitted]. *) -let get_terminator (ps, _) = CEphemeron.get ps.terminator -let set_terminator hook (ps, psl) = - { ps with terminator = CEphemeron.create hook }, psl - -let copy_terminators ~src ~tgt = - let (ps, psl), (ts,tsl) = src, tgt in - assert(List.length psl = List.length tsl); - {ts with terminator = ps.terminator}, List.map2 (fun op p -> { p with terminator = op.terminator }) psl tsl - -let update_global_env (pf : t) = - let res, () = - with_current_proof (fun _ p -> - Proof.in_proof p (fun sigma -> - let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in - let (p,(status,info),()) = Proof.run_tactic (Global.env ()) tac p in - (p, ()))) pf - in res + (Future.from_val ~fix_exn (return_proof ps)) ps + +let update_global_env = + map_proof (fun p -> + Proof.in_proof p (fun sigma -> + let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in + let p,(status,info),_ = Proof.run_tactic (Global.env ()) tac p in + p)) diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index e2e457483b..162f02b654 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.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,14 +13,16 @@ environment. *) type t -val get_current_proof_name : t -> Names.Id.t -val get_current_persistence : t -> Decl_kinds.goal_kind -val get_all_proof_names : t -> Names.Id.t list -val discard : Names.lident -> t -> t option -val discard_current : t -> t option +(* Should be moved into a proper view *) +val get_proof : t -> Proof.t +val get_proof_name : t -> Names.Id.t +val get_persistence : t -> Decl_kinds.goal_kind +val get_used_variables : t -> Constr.named_context option + +(** Get the universe declaration associated to the current proof. *) +val get_universe_decl : t -> UState.universe_decl -val give_me_the_proof : t -> Proof.t val compact_the_proof : t -> t (** When a proof is closed, it is reified into a [proof_object], where @@ -33,26 +35,14 @@ type lemma_possible_guards = int list list type proof_object = { id : Names.Id.t; - entries : Safe_typing.private_constants Entries.definition_entry list; + entries : Evd.side_effects Entries.definition_entry list; persistence : Decl_kinds.goal_kind; universes: UState.t; } type opacity_flag = Opaque | Transparent -type proof_ending = - | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * - UState.t - | Proved of opacity_flag * - Names.lident option * - proof_object -type proof_terminator -type closed_proof = proof_object * proof_terminator - -val make_terminator : (proof_ending -> unit) -> proof_terminator -val apply_terminator : proof_terminator -> proof_ending -> unit - -(** [start_proof ~ontop id str pl goals terminator] starts a proof of name +(** [start_proof id str pl goals] starts a proof of name [id] with goals [goals] (a list of pairs of environment and conclusion); [str] describes what kind of theorem/definition this is; [terminator] is used at the end of the proof to close the proof @@ -60,16 +50,22 @@ val apply_terminator : proof_terminator -> proof_ending -> unit morphism). The proof is started in the evar map [sigma] (which can typically contain universe constraints), and with universe bindings pl. *) -val start_proof : ontop:t option -> - Evd.evar_map -> Names.Id.t -> ?pl:UState.universe_decl -> - Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list -> - proof_terminator -> t +val start_proof + : Evd.evar_map + -> Names.Id.t + -> ?pl:UState.universe_decl + -> Decl_kinds.goal_kind + -> (Environ.env * EConstr.types) list + -> t (** Like [start_proof] except that there may be dependencies between initial goals. *) -val start_dependent_proof : ontop:t option -> - Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind -> - Proofview.telescope -> proof_terminator -> t +val start_dependent_proof + : Names.Id.t + -> ?pl:UState.universe_decl + -> Decl_kinds.goal_kind + -> Proofview.telescope + -> t (** Update the proofs global environment after a side-effecting command (e.g. a sublemma definition) has been run inside it. Assumes @@ -78,33 +74,25 @@ val update_global_env : t -> t (* Takes a function to add to the exceptions data relative to the state in which the proof was built *) -val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> t -> closed_proof +val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> t -> proof_object (* Intermediate step necessary to delegate the future. * Both access the current proof state. The former is supposed to be * chained with a computation that completed the proof *) -type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t +type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t (* If allow_partial is set (default no) then an incomplete proof * is allowed (no error), and a warn is given if the proof is complete. *) val return_proof : ?allow_partial:bool -> t -> closed_proof_output val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> t -> - closed_proof_output Future.computation -> closed_proof + closed_proof_output Future.computation -> proof_object -(** Gets the current terminator without checking that the proof has - been completed. Useful for the likes of [Admitted]. *) -val get_terminator : t -> proof_terminator -val set_terminator : proof_terminator -> t -> t val get_open_goals : t -> int -(** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is - no current proof. - The return boolean is set to [false] if an unsafe tactic has been used. *) -val with_current_proof : - (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a -val simple_with_current_proof : - (unit Proofview.tactic -> Proof.t -> Proof.t) -> t -> t +val map_proof : (Proof.t -> Proof.t) -> t -> t +val map_fold_proof : (Proof.t -> Proof.t * 'a) -> t -> t * 'a +val map_fold_proof_endline : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a (** Sets the tactic to be used when a tactic line is closed with [...] *) val set_endline_tactic : Genarg.glob_generic_argument -> t -> t @@ -114,10 +102,3 @@ val set_endline_tactic : Genarg.glob_generic_argument -> t -> t * ids to be cleared *) val set_used_variables : t -> Names.Id.t list -> (Constr.named_context * Names.lident list) * t - -val get_used_variables : t -> Constr.named_context option - -(** Get the universe declaration associated to the current proof. *) -val get_universe_decl : t -> UState.universe_decl - -val copy_terminators : src:t -> tgt:t -> t diff --git a/proofs/refine.ml b/proofs/refine.ml index 4a9404aa96..dd8b52e56c 100644 --- a/proofs/refine.ml +++ b/proofs/refine.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 *) @@ -60,7 +60,7 @@ let generic_refine ~typecheck f gl = let evs = Evd.save_future_goals sigma in (* Redo the effects in sigma in the monad's env *) let privates_csts = Evd.eval_side_effects sigma in - let env = Safe_typing.push_private_constants env privates_csts in + let env = Safe_typing.push_private_constants env privates_csts.Evd.seff_private in (* Check that the introduced evars are well-typed *) let fold accu ev = typecheck_evar ev env accu in let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in @@ -116,9 +116,6 @@ let lift c = let make_refine_enter ~typecheck f gl = generic_refine ~typecheck (lift f) gl -let refine_one ~typecheck f = - Proofview.Goal.enter_one (make_refine_enter ~typecheck f) - let refine ~typecheck f = let f evd = let (evd,c) = f evd in (evd,((), c)) diff --git a/proofs/refine.mli b/proofs/refine.mli index 55dafe521f..bdcccae805 100644 --- a/proofs/refine.mli +++ b/proofs/refine.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 *) @@ -9,7 +9,7 @@ (************************************************************************) (** The primitive refine tactic used to fill the holes in partial proofs. This - is the recommanded way to write tactics when the proof term is easy to + is the recommended way to write tactics when the proof term is easy to write down. Note that this is not the user-level refine tactic defined in Ltac which is actually based on the one below. *) @@ -27,9 +27,6 @@ val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> uni raised during the interpretation of [t] are caught and result in tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *) -val refine_one : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr.t)) -> 'a tactic -(** A variant of [refine] which assumes exactly one goal under focus *) - val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic -> Proofview.Goal.t -> 'a tactic (** The general version of refine. *) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index bce227dabb..e1896d51e3 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.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 *) @@ -129,9 +129,6 @@ let tclTHENSLASTn tac1 tac taci = tclTHENS3PARTS tac1 [||] tac taci let tclTHEN_i tac taci gls = finish_tac (thensi_tac taci (then_tac tac (start_tac gls))) -let tclTHENLASTn tac1 taci = tclTHENSLASTn tac1 tclIDTAC taci -let tclTHENFIRSTn tac1 taci = tclTHENSFIRSTn tac1 taci tclIDTAC - (* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies [tac2] to every resulting subgoals *) let tclTHEN tac1 tac2 = tclTHENS3PARTS tac1 [||] tac2 [||] @@ -253,46 +250,9 @@ let rec tclFIRST = function | [] -> tclFAIL_s "No applicable tactic." | t::rest -> tclORELSE0 t (tclFIRST rest) -let ite_gen tcal tac_if continue tac_else gl= - let success=ref false in - let tac_if0 gl= - let result=tac_if gl in - success:=true;result in - let tac_else0 e gl= - if !success then - iraise e - else - try - tac_else gl - with - e' when CErrors.noncritical e' -> iraise e in - try - tcal tac_if0 continue gl - with (* Breakpoint *) - | e when CErrors.noncritical e -> - let e = CErrors.push e in catch_failerror e; tac_else0 e gl - -(* Try the first tactic and, if it succeeds, continue with - the second one, and if it fails, use the third one *) - -let tclIFTHENELSE=ite_gen tclTHEN - -(* Idem with tclTHENS and tclTHENSV *) - -let tclIFTHENSELSE=ite_gen tclTHENS - -let tclIFTHENSVELSE=ite_gen tclTHENSV - -let tclIFTHENTRYELSEMUST tac1 tac2 gl = - tclIFTHENELSE tac1 (tclTRY tac2) tac2 gl - (* Fails if a tactic did not solve the goal *) let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.") -(* Try the first thats solves the current goal *) -let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl) - - (* Iteration tacticals *) let tclDO n t = @@ -311,22 +271,7 @@ let rec tclREPEAT t g = let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t)) -(* Repeat on the first subgoal (no failure if no more subgoal) *) -let rec tclREPEAT_MAIN t g = - (tclORELSE (tclTHEN_i t (fun i -> if Int.equal i 1 then (tclREPEAT_MAIN t) else - tclIDTAC)) tclIDTAC) g - (* Change evars *) let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} - -let tclEVARUNIVCONTEXT ctx gls = tclIDTAC {gls with sigma= Evd.set_universe_context gls.sigma ctx} - -(* Push universe context *) -let tclPUSHCONTEXT rigid ctx tac gl = - tclTHEN (tclEVARS (Evd.merge_context_set rigid (project gl) ctx)) tac gl - let tclPUSHEVARUNIVCONTEXT ctx gl = tclEVARS (Evd.merge_universe_context (project gl) ctx) gl - -let tclPUSHCONSTRAINTS cst gl = - tclEVARS (Evd.add_constraints (project gl) cst) gl diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 52cbf7658b..7f8e24fc0e 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.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 *) @@ -32,12 +32,8 @@ val tclIDTAC_MESSAGE : Pp.t -> tactic (** [tclEVARS sigma] changes the current evar map *) val tclEVARS : evar_map -> tactic -val tclEVARUNIVCONTEXT : UState.t -> tactic - -val tclPUSHCONTEXT : Evd.rigid -> Univ.ContextSet.t -> tactic -> tactic val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic -val tclPUSHCONSTRAINTS : Univ.Constraint.t -> tactic (** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies [tac2] to every resulting subgoals *) @@ -86,16 +82,6 @@ val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic [tac2] for the remaining last subgoals (previously called tclTHENST) *) val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic -(** [tclTHENLASTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then, - applies [t1],...,[tn] on the last [n] resulting subgoals and leaves - unchanged the other subgoals *) -val tclTHENLASTn : tactic -> tactic array -> tactic - -(** [tclTHENFIRSTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then, - applies [t1],...,[tn] on the first [n] resulting subgoals and leaves - unchanged the other subgoals (previously called [tclTHENSI]) *) -val tclTHENFIRSTn : tactic -> tactic array -> tactic - (** A special exception for levels for the Fail tactic *) exception FailError of int * Pp.t Lazy.t @@ -106,9 +92,7 @@ val catch_failerror : Exninfo.iexn -> unit val tclORELSE0 : tactic -> tactic -> tactic val tclORELSE : tactic -> tactic -> tactic val tclREPEAT : tactic -> tactic -val tclREPEAT_MAIN : tactic -> tactic val tclFIRST : tactic list -> tactic -val tclSOLVE : tactic list -> tactic val tclTRY : tactic -> tactic val tclTHENTRY : tactic -> tactic -> tactic val tclCOMPLETE : tactic -> tactic @@ -118,16 +102,3 @@ val tclFAIL_lazy : int -> Pp.t Lazy.t -> tactic val tclDO : int -> tactic -> tactic val tclPROGRESS : tactic -> tactic val tclSHOWHYPS : tactic -> tactic - -(** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then, - if it succeeds, applies [tac2] to the resulting subgoals, - and if not applies [tac3] to the initial goal [gls] *) -val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic -val tclIFTHENSELSE : tactic -> tactic list -> tactic ->tactic -val tclIFTHENSVELSE : tactic -> tactic array -> tactic ->tactic - -(** [tclIFTHENTRYELSEMUST tac1 tac2 gls] applies [tac1] then [tac2]. If [tac1] - has been successful, then [tac2] may fail. Otherwise, [tac2] must succeed. - Equivalent to [(tac1;try tac2)||tac2] *) - -val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 93031c2202..d3bce07814 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.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 *) @@ -81,12 +81,10 @@ let pf_type_of = pf_reduce type_of let pf_get_type_of = pf_reduce Retyping.get_type_of let pf_conv_x gl = pf_reduce test_conversion gl Reduction.CONV -let pf_conv_x_leq gl = pf_reduce test_conversion gl Reduction.CUMUL let pf_const_value = pf_reduce (fun env _ c -> EConstr.of_constr (constant_value_in env c)) let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind - let pf_hnf_type_of gls = pf_get_type_of gls %> pf_whd_all gls (* Pretty-printers *) @@ -181,14 +179,7 @@ module New = struct let pf_hnf_type_of gl t = pf_whd_all gl (pf_get_type_of gl t) - let pf_whd_all gl t = pf_apply whd_all gl t let pf_compute gl t = pf_apply compute gl t let pf_nf_evar gl t = nf_evar (project gl) t - - let pf_undefined_evars gl = - let sigma = Proofview.Goal.sigma gl in - let ev = Proofview.Goal.goal gl in - let evi = Evd.find sigma ev in - Evarutil.filtered_undefined_evars_of_evar_info sigma evi end diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 23e1e6f566..def67abad7 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.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 *) @@ -64,7 +64,6 @@ val pf_unfoldn : (occurrences * evaluable_global_reference) list val pf_const_value : Goal.goal sigma -> pconstant -> constr val pf_conv_x : Goal.goal sigma -> constr -> constr -> bool -val pf_conv_x_leq : Goal.goal sigma -> constr -> constr -> bool (** {6 Pretty-printing functions (debug only). } *) val pr_gls : Goal.goal sigma -> Pp.t @@ -109,11 +108,8 @@ module New : sig val pf_hnf_constr : Proofview.Goal.t -> constr -> types val pf_hnf_type_of : Proofview.Goal.t -> constr -> types - val pf_whd_all : Proofview.Goal.t -> constr -> constr val pf_compute : Proofview.Goal.t -> constr -> constr val pf_nf_evar : Proofview.Goal.t -> constr -> constr - (** Gathers the undefined evars of the given goal. *) - val pf_undefined_evars : Proofview.Goal.t -> Evar.Set.t end diff --git a/proofs/tactypes.ml b/proofs/tactypes.ml index 86a7e9c527..634faf1acc 100644 --- a/proofs/tactypes.ml +++ b/proofs/tactypes.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 *) |