aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml10
-rw-r--r--proofs/clenv.mli18
-rw-r--r--proofs/clenvtac.ml12
-rw-r--r--proofs/clenvtac.mli10
-rw-r--r--proofs/evar_refiner.ml10
-rw-r--r--proofs/evar_refiner.mli10
-rw-r--r--proofs/goal.ml10
-rw-r--r--proofs/goal.mli10
-rw-r--r--proofs/logic.ml10
-rw-r--r--proofs/logic.mli10
-rw-r--r--proofs/miscprint.ml10
-rw-r--r--proofs/miscprint.mli10
-rw-r--r--proofs/pfedit.ml10
-rw-r--r--proofs/pfedit.mli10
-rw-r--r--proofs/proof.ml12
-rw-r--r--proofs/proof.mli10
-rw-r--r--proofs/proof_bullet.ml10
-rw-r--r--proofs/proof_bullet.mli10
-rw-r--r--proofs/proof_global.ml13
-rw-r--r--proofs/proof_global.mli13
-rw-r--r--proofs/proof_type.ml10
-rw-r--r--proofs/redexpr.ml10
-rw-r--r--proofs/redexpr.mli10
-rw-r--r--proofs/refine.ml14
-rw-r--r--proofs/refine.mli12
-rw-r--r--proofs/refiner.ml10
-rw-r--r--proofs/refiner.mli10
-rw-r--r--proofs/tacmach.ml16
-rw-r--r--proofs/tacmach.mli58
29 files changed, 212 insertions, 156 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 9e06d913b7..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
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 5ff5fa38ad..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
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 fc94a10132..d713b0999a 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 =
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 bdcb4868bf..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
@@ -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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 01:04:05 +0000