diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 12 | ||||
| -rw-r--r-- | proofs/clenv.mli | 18 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 12 | ||||
| -rw-r--r-- | proofs/clenvtac.mli | 10 | ||||
| -rw-r--r-- | proofs/evar_refiner.ml | 10 | ||||
| -rw-r--r-- | proofs/evar_refiner.mli | 10 | ||||
| -rw-r--r-- | proofs/goal.ml | 10 | ||||
| -rw-r--r-- | proofs/goal.mli | 10 | ||||
| -rw-r--r-- | proofs/logic.ml | 14 | ||||
| -rw-r--r-- | proofs/logic.mli | 10 | ||||
| -rw-r--r-- | proofs/miscprint.ml | 10 | ||||
| -rw-r--r-- | proofs/miscprint.mli | 10 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 10 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 10 | ||||
| -rw-r--r-- | proofs/proof.ml | 12 | ||||
| -rw-r--r-- | proofs/proof.mli | 10 | ||||
| -rw-r--r-- | proofs/proof_bullet.ml | 10 | ||||
| -rw-r--r-- | proofs/proof_bullet.mli | 10 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 35 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 13 | ||||
| -rw-r--r-- | proofs/proof_type.ml | 10 | ||||
| -rw-r--r-- | proofs/redexpr.ml | 10 | ||||
| -rw-r--r-- | proofs/redexpr.mli | 10 | ||||
| -rw-r--r-- | proofs/refine.ml | 14 | ||||
| -rw-r--r-- | proofs/refine.mli | 12 | ||||
| -rw-r--r-- | proofs/refiner.ml | 10 | ||||
| -rw-r--r-- | proofs/refiner.mli | 10 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 18 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 58 |
29 files changed, 228 insertions, 170 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 16798a1d57..54ba19d6a9 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -498,7 +500,7 @@ let clenv_unify_binding_type clenv c t u = let clenv_assign_binding clenv k c = let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in - let c_typ = nf_betaiota clenv.evd (clenv_get_type_of clenv c) in + let c_typ = nf_betaiota clenv.env clenv.evd (clenv_get_type_of clenv c) in let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in let c = EConstr.Unsafe.to_constr c in { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd } diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 9a2026dd37..b85c4fc51b 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This file defines clausenv, which is a deprecated way to handle open terms @@ -41,10 +43,10 @@ val clenv_nf_meta : clausenv -> EConstr.constr -> EConstr.constr (** type of a meta in clenv context *) val clenv_meta_type : clausenv -> metavariable -> types -val mk_clenv_from : 'a Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv +val mk_clenv_from : Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv val mk_clenv_from_n : - 'a Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv -val mk_clenv_type_of : 'a Proofview.Goal.t -> EConstr.constr -> clausenv + Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv +val mk_clenv_type_of : Proofview.Goal.t -> EConstr.constr -> clausenv val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv (** Refresh the universes in a clenv *) @@ -66,7 +68,7 @@ val old_clenv_unique_resolver : ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv val clenv_unique_resolver : - ?flags:unify_flags -> clausenv -> 'a Proofview.Goal.t -> clausenv + ?flags:unify_flags -> clausenv -> Proofview.Goal.t -> clausenv val clenv_dependent : clausenv -> metavariable list diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 8bd5d98cb9..209104ac32 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util @@ -141,7 +143,7 @@ let fail_quick_unif_flags = { let unify ?(flags=fail_quick_unif_flags) m = Proofview.Goal.enter begin fun gl -> let env = Tacmach.New.pf_env gl in - let n = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in + let n = Tacmach.New.pf_concl gl in let evd = clear_metas (Tacmach.New.project gl) in try let evd' = w_unify env evd CONV ~flags m n in diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index 7c3577e345..7c1e300b8f 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Legacy components of the previous proof engine. *) diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index d38ff7512f..0d197c92c5 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index d90cff5722..e8f3c4d173 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Evd diff --git a/proofs/goal.ml b/proofs/goal.ml index d5bc7e0ce2..ed0d76f93a 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util diff --git a/proofs/goal.mli b/proofs/goal.mli index 37dd9d3c0c..dc9863156c 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This module implements the abstract interface to goals. Most of the code diff --git a/proofs/logic.ml b/proofs/logic.ml index 1d86a09092..e5294715e0 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -334,7 +336,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = else match kind trm with | Meta _ -> - let conclty = nf_betaiota sigma (EConstr.of_constr conclty) in + let conclty = nf_betaiota env sigma (EConstr.of_constr conclty) in if !check && occur_meta sigma conclty then raise (RefinerError (env, sigma, MetaInType conclty)); let (gl,ev,sigma) = mk_goal hyps conclty in @@ -416,7 +418,7 @@ and mk_hdgoals sigma goal goalacc trm = match kind trm with | Cast (c,_, ty) when isMeta c -> check_typability env sigma ty; - let (gl,ev,sigma) = mk_goal hyps (nf_betaiota sigma (EConstr.of_constr ty)) in + let (gl,ev,sigma) = mk_goal hyps (nf_betaiota env sigma (EConstr.of_constr ty)) in let ev = EConstr.Unsafe.to_constr ev in gl::goalacc,ty,sigma,ev diff --git a/proofs/logic.mli b/proofs/logic.mli index afd1ecf70b..dc471bb5fe 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Legacy proof engine. Do not use in newly written code. *) diff --git a/proofs/miscprint.ml b/proofs/miscprint.ml index 92b58b4092..e363af644f 100644 --- a/proofs/miscprint.ml +++ b/proofs/miscprint.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp diff --git a/proofs/miscprint.mli b/proofs/miscprint.mli index b75718cd01..762d7cc877 100644 --- a/proofs/miscprint.mli +++ b/proofs/miscprint.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Misctypes diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 6b503a0112..03babfede2 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 5a317a956d..65cde3a3ae 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Global proof state. A quite redundant wrapper on {!Proof_global}. *) diff --git a/proofs/proof.ml b/proofs/proof.ml index 04e707cd66..24f570f01e 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Module defining the last essential tiles of interactive proofs. @@ -432,7 +434,7 @@ module V82 = struct CList.nth evl (n-1) in let env = Evd.evar_filtered_env evi in - let rawc = Constrintern.intern_constr env com in + let rawc = Constrintern.intern_constr env sigma com in let ltac_vars = Glob_ops.empty_lvar in let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in Proofview.Unsafe.tclEVARS sigma diff --git a/proofs/proof.mli b/proofs/proof.mli index 0b5e771ef3..c0e832fb8c 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Module defining the last essential tiles of interactive proofs. diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index 2149163314..e22d382f7d 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Proof diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli index 09fcabf50a..ffbaa0fac9 100644 --- a/proofs/proof_bullet.mli +++ b/proofs/proof_bullet.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (**********************************************************) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 167d6bda0d..8b5b739a33 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (***********************************************************************) @@ -79,7 +81,7 @@ type proof_object = { type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t | Proved of Vernacexpr.opacity_flag * - Vernacexpr.lident option * + Misctypes.lident option * proof_object type proof_terminator = proof_ending -> unit type closed_proof = proof_object * proof_terminator @@ -146,6 +148,7 @@ let cur_pstate () = | [] -> raise NoCurrentProof let give_me_the_proof () = (cur_pstate ()).proof +let give_me_the_proof_opt () = try Some (give_me_the_proof ()) with | NoCurrentProof -> None let get_current_proof_name () = (cur_pstate ()).pid let with_current_proof f = @@ -338,21 +341,20 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let subst_evar k = Proof.in_proof proof (fun m -> Evd.existential_opt_value m k) in let nf = Universes.nf_evars_and_universes_opt_subst subst_evar - (Evd.evar_universe_context_subst universes) in + (UState.subst universes) in let make_body = if poly || now then let make_body t (c, eff) = let body = c in - let typ = - if not (keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff)) then - nf t - else t + let allow_deferred = + not poly && (keep_body_ucst_separate || + not (Safe_typing.empty_private_constants = eff)) in + let typ = if allow_deferred then t else nf t in let env = Global.env () in let used_univs_body = Univops.universes_of_constr env body in let used_univs_typ = Univops.universes_of_constr env typ in - if keep_body_ucst_separate || - not (Safe_typing.empty_private_constants = eff) then + if allow_deferred then let initunivs = UState.const_univ_entry ~poly initial_euctx in let ctx = constrain_variables universes in (* For vi2vo compilation proofs are computed now but we need to @@ -434,7 +436,7 @@ let return_proof ?(allow_partial=false) () = | Proof.HasUnresolvedEvar-> error(strbrk"Attempt to save a proof with existential variables still non-instantiated") in let eff = Evd.eval_side_effects evd in - let evd = Evd.nf_constraints evd in + let evd = Evd.minimize_universes evd in (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects thereafter... *) @@ -486,7 +488,10 @@ let update_global_env () = (* XXX: Bullet hook, should be really moved elsewhere *) let _ = let hook n = - let prf = give_me_the_proof () in - (Proof_bullet.suggest prf) in + try + let prf = give_me_the_proof () in + (Proof_bullet.suggest prf) + with NoCurrentProof -> mt () + in Proofview.set_nosuchgoals_hook hook diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 27e99f218b..fb123fccb3 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This module defines proof facilities relevant to the @@ -24,6 +26,7 @@ val discard : Names.Id.t Loc.located -> unit val discard_current : unit -> unit val discard_all : unit -> unit +val give_me_the_proof_opt : unit -> Proof.t option exception NoCurrentProof val give_me_the_proof : unit -> Proof.t (** @raise NoCurrentProof when outside proof mode. *) @@ -49,7 +52,7 @@ type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t | Proved of Vernacexpr.opacity_flag * - Vernacexpr.lident option * + Misctypes.lident option * proof_object type proof_terminator type closed_proof = proof_object * proof_terminator diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 20293cb9b3..149f30c673 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Legacy proof engine. Do not use in newly written code. *) diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 9a5d4e154e..6fb4119387 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli index 43e5987733..1e59f436c3 100644 --- a/proofs/redexpr.mli +++ b/proofs/redexpr.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Interpretation layer of redexprs such as hnf, cbv, etc. *) diff --git a/proofs/refine.ml b/proofs/refine.ml index e3f6508481..50fd1c4722 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util @@ -70,10 +72,10 @@ let add_side_effects env effects = List.fold_left (fun env eff -> add_side_effect env eff) env effects let generic_refine ~typecheck f gl = - let gl = Proofview.Goal.assume gl in let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in + let state = Proofview.Goal.state gl in (** Save the [future_goals] state to restore them after the refinement. *) let prev_future_goals = Evd.future_goals sigma in @@ -121,6 +123,7 @@ let generic_refine ~typecheck f gl = (** Select the goals *) let comb = CList.map_filter (Proofview.Unsafe.advance sigma) (CList.rev evs) in let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in + let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in let trace () = Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)) in Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v -> Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*> @@ -159,7 +162,6 @@ let with_type env evd c t = evd , j'.Environ.uj_val let refine_casted ~typecheck f = Proofview.Goal.enter begin fun gl -> - let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let f h = diff --git a/proofs/refine.mli b/proofs/refine.mli index cfdcde36e0..70a23a9fba 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** The primitive refine tactic used to fill the holes in partial proofs. This @@ -33,7 +35,7 @@ val refine_one : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr (** A variant of [refine] which assumes exactly one goal under focus *) val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic -> - [ `NF ] Proofview.Goal.t -> 'a tactic + Proofview.Goal.t -> 'a tactic (** The general version of refine. *) (** {7 Helper functions} *) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index cd2b109061..be32aadd91 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 52dc8bfd8c..5cd703a25c 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Legacy proof engine. Do not use in newly written code. *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index d415412510..1889054f86 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util @@ -87,7 +89,7 @@ let pf_e_reduce = pf_apply let pf_whd_all = pf_reduce whd_all let pf_hnf_constr = pf_reduce hnf_constr let pf_nf = pf_reduce simpl -let pf_nf_betaiota = pf_reduce (fun _ -> nf_betaiota) +let pf_nf_betaiota = pf_reduce nf_betaiota let pf_compute = pf_reduce compute let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds) let pf_unsafe_type_of = pf_reduce unsafe_type_of @@ -150,7 +152,6 @@ module New = struct let pf_global id gl = (** We only check for the existence of an [id] in [hyps] *) - let gl = Proofview.Goal.assume gl in let hyps = Proofview.Goal.hyps gl in Constrintern.construct_reference hyps id @@ -167,13 +168,11 @@ module New = struct let pf_ids_of_hyps gl = (** We only get the identifiers in [hyps] *) - let gl = Proofview.Goal.assume gl in let hyps = Proofview.Goal.hyps gl in ids_of_named_context hyps let pf_ids_set_of_hyps gl = (** We only get the identifiers in [hyps] *) - let gl = Proofview.Goal.assume gl in let env = Proofview.Goal.env gl in Environ.ids_of_named_context_val (Environ.named_context_val env) @@ -204,9 +203,8 @@ module New = struct let hyps = Proofview.Goal.hyps gl in List.hd hyps - let pf_nf_concl (gl : [ `LZ ] Proofview.Goal.t) = + let pf_nf_concl (gl : Proofview.Goal.t) = (** We normalize the conclusion just after *) - let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in let sigma = project gl in nf_evar sigma concl diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index e0fb8fbc5d..770d0940a3 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -92,46 +94,46 @@ val pr_glls : goal list sigma -> Pp.t (* Variants of [Tacmach] functions built with the new proof engine *) module New : sig - val pf_apply : (env -> evar_map -> 'a) -> 'b Proofview.Goal.t -> 'a - val pf_global : Id.t -> 'a Proofview.Goal.t -> Globnames.global_reference + val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a + val pf_global : Id.t -> Proofview.Goal.t -> Globnames.global_reference (** FIXME: encapsulate the level in an existential type. *) - val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a + val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a - val project : 'a Proofview.Goal.t -> Evd.evar_map - val pf_env : 'a Proofview.Goal.t -> Environ.env - val pf_concl : 'a Proofview.Goal.t -> types + val project : Proofview.Goal.t -> Evd.evar_map + val pf_env : Proofview.Goal.t -> Environ.env + val pf_concl : Proofview.Goal.t -> types (** WRONG: To be avoided at all costs, it typechecks the term entirely but forgets the universe constraints necessary to retypecheck it *) - val pf_unsafe_type_of : 'a Proofview.Goal.t -> constr -> types + val pf_unsafe_type_of : Proofview.Goal.t -> constr -> types (** This function does no type inference and expects an already well-typed term. It recomputes its type in the fastest way possible (no conversion is ever involved) *) - val pf_get_type_of : 'a Proofview.Goal.t -> constr -> types + val pf_get_type_of : Proofview.Goal.t -> constr -> types (** This function entirely type-checks the term and computes its type and the implied universe constraints. *) - val pf_type_of : 'a Proofview.Goal.t -> constr -> evar_map * types - val pf_conv_x : 'a Proofview.Goal.t -> t -> t -> bool + val pf_type_of : Proofview.Goal.t -> constr -> evar_map * types + val pf_conv_x : Proofview.Goal.t -> t -> t -> bool - val pf_get_new_id : Id.t -> 'a Proofview.Goal.t -> Id.t - val pf_ids_of_hyps : 'a Proofview.Goal.t -> Id.t list - val pf_ids_set_of_hyps : 'a Proofview.Goal.t -> Id.Set.t - val pf_hyps_types : 'a Proofview.Goal.t -> (Id.t * types) list + val pf_get_new_id : Id.t -> Proofview.Goal.t -> Id.t + val pf_ids_of_hyps : Proofview.Goal.t -> Id.t list + val pf_ids_set_of_hyps : Proofview.Goal.t -> Id.Set.t + val pf_hyps_types : Proofview.Goal.t -> (Id.t * types) list - val pf_get_hyp : Id.t -> 'a Proofview.Goal.t -> named_declaration - val pf_get_hyp_typ : Id.t -> 'a Proofview.Goal.t -> types - val pf_last_hyp : 'a Proofview.Goal.t -> named_declaration + val pf_get_hyp : Id.t -> Proofview.Goal.t -> named_declaration + val pf_get_hyp_typ : Id.t -> Proofview.Goal.t -> types + val pf_last_hyp : Proofview.Goal.t -> named_declaration - val pf_nf_concl : [ `LZ ] Proofview.Goal.t -> types - val pf_reduce_to_quantified_ind : 'a Proofview.Goal.t -> types -> (inductive * EInstance.t) * types + val pf_nf_concl : Proofview.Goal.t -> types + val pf_reduce_to_quantified_ind : Proofview.Goal.t -> types -> (inductive * EInstance.t) * types - val pf_hnf_constr : 'a Proofview.Goal.t -> constr -> types - val pf_hnf_type_of : 'a Proofview.Goal.t -> constr -> types + val pf_hnf_constr : Proofview.Goal.t -> constr -> types + val pf_hnf_type_of : Proofview.Goal.t -> constr -> types - val pf_whd_all : 'a Proofview.Goal.t -> constr -> constr - val pf_compute : 'a Proofview.Goal.t -> constr -> constr + val pf_whd_all : Proofview.Goal.t -> constr -> constr + val pf_compute : Proofview.Goal.t -> constr -> constr - val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr + val pf_nf_evar : Proofview.Goal.t -> constr -> constr end |