aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.circleci/config.yml4
-rw-r--r--.github/CODEOWNERS5
-rw-r--r--.gitlab-ci.yml3
-rw-r--r--.travis.yml13
-rw-r--r--Makefile.ci1
-rwxr-xr-xdev/ci/ci-basic-overlay.sh6
-rwxr-xr-xdev/ci/ci-pidetop.sh13
-rw-r--r--parsing/g_vernac.ml41
-rw-r--r--plugins/ltac/g_ltac.ml42
-rw-r--r--plugins/ltac/pptactic.mli2
-rw-r--r--plugins/ltac/tacexpr.ml4
-rw-r--r--plugins/ltac/tacexpr.mli4
-rw-r--r--pretyping/vernacexpr.ml27
-rw-r--r--printing/ppvernac.ml11
-rw-r--r--proofs/goal_select.ml68
-rw-r--r--proofs/goal_select.mli26
-rw-r--r--proofs/pfedit.ml14
-rw-r--r--proofs/pfedit.mli2
-rw-r--r--proofs/proof_bullet.ml70
-rw-r--r--proofs/proof_bullet.mli19
-rw-r--r--proofs/proof_global.ml1
-rw-r--r--proofs/proofs.mllib1
-rw-r--r--stm/proofBlockDelimiter.ml4
-rw-r--r--stm/proofBlockDelimiter.mli4
-rw-r--r--stm/stm.ml2
-rw-r--r--tactics/tacticals.ml12
-rw-r--r--tactics/tacticals.mli2
-rw-r--r--tools/CoqMakefile.in2
-rw-r--r--toplevel/coqtop.ml20
-rw-r--r--vernac/vernacentries.ml6
30 files changed, 219 insertions, 130 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml
index f811f26e1..451b711be 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -209,6 +209,9 @@ jobs:
mtac2:
<<: *ci-template
+ pidetop:
+ <<: *ci-template
+
sf:
<<: *ci-template
environment:
@@ -266,6 +269,7 @@ workflows:
- iris-lambda-rust: *req-main
- ltac2: *req-main
- math-comp: *req-main
+ - pidetop: *req-main
- sf: *req-main
- unimath: *req-main
- vst: *req-main
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index 329697ca4..74bbda553 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -303,9 +303,12 @@
# Secondary maintainer @maximedenes
# This file belongs to CI
-Makefile.ci @ejgallego
+/Makefile.ci @ejgallego
# Secondary maintainer @SkySkimmer
+/Makefile.doc @maximedenes
+# Secondary maintainer @silene
+
########## Developer tools ##########
/dev/tools/backport-pr.sh @Zimmi48
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 6b42ac7eb..d16dc5b78 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -363,6 +363,9 @@ ci-math-comp:
ci-mtac2:
<<: *ci-template
+ci-pidetop:
+ <<: *ci-template
+
ci-sf:
<<: *ci-template
variables:
diff --git a/.travis.yml b/.travis.yml
index a60d68de5..fce19f9d9 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -54,7 +54,7 @@ env:
- TEST_TARGET="test-suite" COMPILER="4.02.3+32bit"
- TEST_TARGET="validate" TW="travis_wait"
- TEST_TARGET="validate" COMPILER="4.02.3+32bit" TW="travis_wait"
- - TEST_TARGET="validate" COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" EXTRA_OPAM="num" FINDLIB_VER="${FINDLIB_VER_BE}"
+ - TEST_TARGET="validate" COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" FINDLIB_VER="${FINDLIB_VER_BE}"
matrix:
@@ -120,6 +120,9 @@ matrix:
- TEST_TARGET="ci-mtac2"
- if: NOT (type = pull_request)
env:
+ - TEST_TARGET="ci-pidetop"
+ - if: NOT (type = pull_request)
+ env:
- TEST_TARGET="ci-sf"
- if: NOT (type = pull_request)
env:
@@ -174,7 +177,7 @@ matrix:
- FINDLIB_VER="${FINDLIB_VER_BE}"
- CAMLP5_VER="${CAMLP5_VER_BE}"
- EXTRA_CONF="-coqide opt -with-doc yes"
- - EXTRA_OPAM="num hevea ${LABLGTK_BE}"
+ - EXTRA_OPAM="hevea ${LABLGTK_BE}"
before_install: *sphinx-install
addons:
apt:
@@ -190,7 +193,7 @@ matrix:
- CAMLP5_VER="${CAMLP5_VER_BE}"
- NATIVE_COMP="no"
- EXTRA_CONF="-coqide opt -with-doc yes -flambda-opts -O3"
- - EXTRA_OPAM="num hevea ${LABLGTK_BE}"
+ - EXTRA_OPAM="hevea ${LABLGTK_BE}"
before_install: *sphinx-install
addons:
apt:
@@ -219,7 +222,7 @@ matrix:
- FINDLIB_VER="${FINDLIB_VER_BE}"
- CAMLP5_VER="${CAMLP5_VER_BE}"
- EXTRA_CONF="-byte-only -coqide byte -warn-error yes"
- - EXTRA_OPAM="num hevea ${LABLGTK_BE}"
+ - EXTRA_OPAM="hevea ${LABLGTK_BE}"
addons:
apt:
sources:
@@ -277,7 +280,7 @@ install:
- opam init -j ${NJOBS} --compiler=${COMPILER} -n -y
- eval $(opam config env)
- opam config list
-- opam install -j ${NJOBS} -y camlp5${CAMLP5_VER} ocamlfind${FINDLIB_VER} ${EXTRA_OPAM}
+- opam install -j ${NJOBS} -y num camlp5${CAMLP5_VER} ocamlfind${FINDLIB_VER} ${EXTRA_OPAM}
- opam list
script:
diff --git a/Makefile.ci b/Makefile.ci
index 37b14ed91..78fec466c 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -29,6 +29,7 @@ CI_TARGETS=ci-bignums \
ci-math-classes \
ci-math-comp \
ci-mtac2 \
+ ci-pidetop \
ci-sf \
ci-tlc \
ci-unimath \
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 5cee72cc7..1ae2ad0ac 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -156,3 +156,9 @@
########################################################################
: "${fcsl_pcm_CI_BRANCH:=master}"
: "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm.git}"
+
+########################################################################
+# pidetop
+########################################################################
+: "${pidetop_CI_BRANCH:=v8.9}"
+: "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop.git}"
diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh
new file mode 100755
index 000000000..d04b9637c
--- /dev/null
+++ b/dev/ci/ci-pidetop.sh
@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+pidetop_CI_DIR="${CI_BUILD_DIR}/pidetop"
+
+git_checkout "${pidetop_CI_BRANCH}" "${pidetop_CI_GITURL}" "${pidetop_CI_DIR}"
+
+( cd "${pidetop_CI_DIR}" && coq_makefile -f Make -o Makefile.top && make -f Makefile.top "-j${NJOBS}" && make install-toploop -f Makefile.top )
+
+echo -en '4\nexit' | coqtop -main-channel stdfds -toploop pidetop
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 2dbd624c2..3026be248 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -48,6 +48,7 @@ let instance_name = Gram.entry_create "vernac:instance_name"
let section_subset_expr = Gram.entry_create "vernac:section_subset_expr"
let make_bullet s =
+ let open Proof_bullet in
let n = String.length s in
match s.[0] with
| '-' -> Dash n
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index a1d7d9b1a..4857beffa 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -416,7 +416,7 @@ let is_explicit_terminator = function TacSolve _ -> true | _ -> false
VERNAC tactic_mode EXTEND VernacSolve
| [ - ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
[ classify_as_proofstep ] -> [
- let g = Option.default (Proof_bullet.get_default_goal_selector ()) g in
+ let g = Option.default (Goal_select.get_default_goal_selector ()) g in
vernac_solve g n t def
]
| [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index aea00c240..799a52cc8 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -84,7 +84,7 @@ type pp_tactic = {
pptac_prods : grammar_terminals;
}
-val pr_goal_selector : toplevel:bool -> Vernacexpr.goal_selector -> Pp.t
+val pr_goal_selector : toplevel:bool -> Goal_select.t -> Pp.t
val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 37abfeee9..17f5e5d41 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -35,7 +35,7 @@ type advanced_flag = bool (* true = advanced false = basic *)
type letin_flag = bool (* true = use local def false = use Leibniz *)
type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
-type goal_selector = Vernacexpr.goal_selector =
+type goal_selector = Goal_select.t =
| SelectAlreadyFocused
| SelectNth of int
| SelectList of (int * int) list
@@ -270,7 +270,7 @@ and 'a gen_tactic_expr =
('p,'a gen_tactic_expr) match_rule list
| TacFun of 'a gen_tactic_fun_ast
| TacArg of 'a gen_tactic_arg located
- | TacSelect of Vernacexpr.goal_selector * 'a gen_tactic_expr
+ | TacSelect of Goal_select.t * 'a gen_tactic_expr
(* For ML extensions *)
| TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located
(* For syntax extensions *)
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 37abfeee9..17f5e5d41 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -35,7 +35,7 @@ type advanced_flag = bool (* true = advanced false = basic *)
type letin_flag = bool (* true = use local def false = use Leibniz *)
type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
-type goal_selector = Vernacexpr.goal_selector =
+type goal_selector = Goal_select.t =
| SelectAlreadyFocused
| SelectNth of int
| SelectList of (int * int) list
@@ -270,7 +270,7 @@ and 'a gen_tactic_expr =
('p,'a gen_tactic_expr) match_rule list
| TacFun of 'a gen_tactic_fun_ast
| TacArg of 'a gen_tactic_arg located
- | TacSelect of Vernacexpr.goal_selector * 'a gen_tactic_expr
+ | TacSelect of Goal_select.t * 'a gen_tactic_expr
(* For ML extensions *)
| TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located
(* For syntax extensions *)
diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml
index 548689205..8bf810498 100644
--- a/pretyping/vernacexpr.ml
+++ b/pretyping/vernacexpr.ml
@@ -16,17 +16,13 @@ open Libnames
(** Vernac expressions, produced by the parser *)
type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation
-(* spiwack: I'm choosing, for now, to have [goal_selector] be a
- different type than [goal_reference] mostly because if it makes sense
- to print a goal that is out of focus (or already solved) it doesn't
- make sense to apply a tactic to it. Hence it the types may look very
- similar, they do not seem to mean the same thing. *)
-type goal_selector =
+type goal_selector = Goal_select.t =
| SelectAlreadyFocused
| SelectNth of int
| SelectList of (int * int) list
| SelectId of Id.t
| SelectAll
+[@@ocaml.deprecated "Use Goal_select.t"]
type goal_identifier = string
type scope_name = string
@@ -69,7 +65,7 @@ type printable =
| PrintScopes
| PrintScope of string
| PrintVisibility of string option
- | PrintAbout of reference or_by_notation * Universes.univ_name_list option * goal_selector option
+ | PrintAbout of reference or_by_notation * Universes.univ_name_list option * Goal_select.t option
| PrintImplicit of reference or_by_notation
| PrintAssumptions of bool * bool * reference or_by_notation
| PrintStrategy of reference or_by_notation option
@@ -198,7 +194,6 @@ type one_inductive_expr =
ident_decl * local_binder_expr list * constr_expr option * constructor_expr list
type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr
-
and typeclass_context = typeclass_constraint list
type proof_expr =
@@ -270,13 +265,11 @@ type extend_name =
(* This type allows registering the inlining of constants in native compiler.
It will be extended with primitive inductive types and operators *)
-type register_kind =
+type register_kind =
| RegisterInline
-type bullet =
- | Dash of int
- | Star of int
- | Plus of int
+type bullet = Proof_bullet.t
+[@@ocaml.deprecated "Alias type, please use [Proof_bullet.t]"]
(** {6 Types concerning the module layer} *)
@@ -426,11 +419,11 @@ type nonrec vernac_expr =
| VernacRemoveOption of Goptions.option_name * option_ref_value list
| VernacMemOption of Goptions.option_name * option_ref_value list
| VernacPrintOption of Goptions.option_name
- | VernacCheckMayEval of Genredexpr.raw_red_expr option * goal_selector option * constr_expr
+ | VernacCheckMayEval of Genredexpr.raw_red_expr option * Goal_select.t option * constr_expr
| VernacGlobalCheck of constr_expr
| VernacDeclareReduction of string * Genredexpr.raw_red_expr
| VernacPrint of printable
- | VernacSearch of searchable * goal_selector option * search_restriction
+ | VernacSearch of searchable * Goal_select.t option * search_restriction
| VernacLocate of locatable
| VernacRegister of lident * register_kind
| VernacComments of comment list
@@ -444,8 +437,8 @@ type nonrec vernac_expr =
| VernacFocus of int option
| VernacUnfocus
| VernacUnfocused
- | VernacBullet of bullet
- | VernacSubproof of goal_selector option
+ | VernacBullet of Proof_bullet.t
+ | VernacSubproof of Goal_select.t option
| VernacEndSubproof
| VernacShow of showable
| VernacCheckGuard
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 83c875707..89117caf4 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -145,7 +145,7 @@ open Pputils
| SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
let pr_search a gopt b pr_p =
- pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt
+ pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt
++
match a with
| SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b
@@ -508,7 +508,7 @@ open Pputils
| PrintVisibility s ->
keyword "Print Visibility" ++ pr_opt str s
| PrintAbout (qid,l,gopt) ->
- pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt
+ pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt
++ keyword "About" ++ spc() ++ pr_smart_global qid ++ pr_univ_name_list l
| PrintImplicit qid ->
keyword "Print Implicit" ++ spc() ++ pr_smart_global qid
@@ -1122,7 +1122,7 @@ open Pputils
| None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c)
in
let pr_i = match io with None -> mt ()
- | Some i -> Proof_bullet.pr_goal_selector i ++ str ": " in
+ | Some i -> Goal_select.pr_goal_selector i ++ str ": " in
return (pr_i ++ pr_mayeval r c)
| VernacGlobalCheck c ->
return (hov 2 (keyword "Type" ++ pr_constrarg c))
@@ -1176,7 +1176,8 @@ open Pputils
| VernacProofMode s ->
return (keyword "Proof Mode" ++ str s)
| VernacBullet b ->
- return (begin match b with
+ (* XXX: Redundant with Proof_bullet.print *)
+ return (let open Proof_bullet in begin match b with
| Dash n -> str (String.make n '-')
| Star n -> str (String.make n '*')
| Plus n -> str (String.make n '+')
@@ -1184,7 +1185,7 @@ open Pputils
| VernacSubproof None ->
return (str "{")
| VernacSubproof (Some i) ->
- return (Proof_bullet.pr_goal_selector i ++ str ":" ++ spc () ++ str "{")
+ return (Goal_select.pr_goal_selector i ++ str ":" ++ spc () ++ str "{")
| VernacEndSubproof ->
return (str "}")
diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml
new file mode 100644
index 000000000..65a94a2c6
--- /dev/null
+++ b/proofs/goal_select.ml
@@ -0,0 +1,68 @@
+(************************************************************************)
+(* * 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 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Names
+
+(* spiwack: I'm choosing, for now, to have [goal_selector] be a
+ different type than [goal_reference] mostly because if it makes sense
+ to print a goal that is out of focus (or already solved) it doesn't
+ make sense to apply a tactic to it. Hence it the types may look very
+ similar, they do not seem to mean the same thing. *)
+type t =
+ | SelectAlreadyFocused
+ | SelectNth of int
+ | SelectList of (int * int) list
+ | SelectId of Id.t
+ | SelectAll
+
+(* Default goal selector: selector chosen when a tactic is applied
+ without an explicit selector. *)
+let default_goal_selector = ref (SelectNth 1)
+let get_default_goal_selector () = !default_goal_selector
+
+let pr_range_selector (i, j) =
+ if i = j then Pp.int i
+ else Pp.(int i ++ str "-" ++ int j)
+
+let pr_goal_selector = function
+ | SelectAlreadyFocused -> Pp.str "!"
+ | SelectAll -> Pp.str "all"
+ | SelectNth i -> Pp.int i
+ | SelectList l ->
+ Pp.(str "["
+ ++ prlist_with_sep pr_comma pr_range_selector l
+ ++ str "]")
+ | SelectId id -> Names.Id.print id
+
+let parse_goal_selector = function
+ | "!" -> SelectAlreadyFocused
+ | "all" -> SelectAll
+ | i ->
+ let err_msg = "The default selector must be \"all\" or a natural number." in
+ begin try
+ let i = int_of_string i in
+ if i < 0 then CErrors.user_err Pp.(str err_msg);
+ SelectNth i
+ with Failure _ -> CErrors.user_err Pp.(str err_msg)
+ end
+
+let _ = let open Goptions in
+ declare_string_option
+ { optdepr = false;
+ optname = "default goal selector" ;
+ optkey = ["Default";"Goal";"Selector"] ;
+ optread = begin fun () ->
+ Pp.string_of_ppcmds
+ (pr_goal_selector !default_goal_selector)
+ end;
+ optwrite = begin fun n ->
+ default_goal_selector := parse_goal_selector n
+ end
+ }
diff --git a/proofs/goal_select.mli b/proofs/goal_select.mli
new file mode 100644
index 000000000..b1c572388
--- /dev/null
+++ b/proofs/goal_select.mli
@@ -0,0 +1,26 @@
+(************************************************************************)
+(* * 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 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Names
+
+(* spiwack: I'm choosing, for now, to have [goal_selector] be a
+ different type than [goal_reference] mostly because if it makes sense
+ to print a goal that is out of focus (or already solved) it doesn't
+ make sense to apply a tactic to it. Hence it the types may look very
+ similar, they do not seem to mean the same thing. *)
+type t =
+ | SelectAlreadyFocused
+ | SelectNth of int
+ | SelectList of (int * int) list
+ | SelectId of Id.t
+ | SelectAll
+
+val pr_goal_selector : t -> Pp.t
+val get_default_goal_selector : unit -> t
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 62a38fa32..03c0969fa 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -100,8 +100,8 @@ let solve ?with_end_tac gi info_lvl tac pr =
| None -> tac
| Some _ -> Proofview.Trace.record_info_trace tac
in
- let tac = match gi with
- | Vernacexpr.SelectAlreadyFocused ->
+ let tac = let open Goal_select in match gi with
+ | SelectAlreadyFocused ->
let open Proofview.Notations in
Proofview.numgoals >>= fun n ->
if n == 1 then tac
@@ -113,10 +113,10 @@ let solve ?with_end_tac gi info_lvl tac pr =
in
Proofview.tclZERO e
- | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac
- | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l tac
- | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac
- | Vernacexpr.SelectAll -> tac
+ | SelectNth i -> Proofview.tclFOCUS i i tac
+ | SelectList l -> Proofview.tclFOCUSLIST l tac
+ | SelectId id -> Proofview.tclFOCUSID id tac
+ | SelectAll -> tac
in
let tac =
if use_unification_heuristics () then
@@ -133,7 +133,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
with
Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof")
-let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac)
+let by tac = Proof_global.with_current_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac)
let instantiate_nth_evar_com n com =
Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.instantiate_evar n com p)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 65cde3a3a..805635dfa 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -75,7 +75,7 @@ val current_proof_statement :
tac] applies [tac] to all subgoals. *)
val solve : ?with_end_tac:unit Proofview.tactic ->
- Vernacexpr.goal_selector -> int option -> unit Proofview.tactic ->
+ Goal_select.t -> int option -> unit Proofview.tactic ->
Proof.t -> Proof.t * bool
(** [by tac] applies tactic [tac] to the 1st subgoal of the current
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index d6f7c0e93..cc3e79f85 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -10,19 +10,22 @@
open Proof
-type t = Vernacexpr.bullet
+type t =
+ | Dash of int
+ | Star of int
+ | Plus of int
let bullet_eq b1 b2 = match b1, b2 with
-| Vernacexpr.Dash n1, Vernacexpr.Dash n2 -> n1 = n2
-| Vernacexpr.Star n1, Vernacexpr.Star n2 -> n1 = n2
-| Vernacexpr.Plus n1, Vernacexpr.Plus n2 -> n1 = n2
+| Dash n1, Dash n2 -> n1 = n2
+| Star n1, Star n2 -> n1 = n2
+| Plus n1, Plus n2 -> n1 = n2
| _ -> false
let pr_bullet b =
match b with
- | Vernacexpr.Dash n -> Pp.(str (String.make n '-'))
- | Vernacexpr.Star n -> Pp.(str (String.make n '*'))
- | Vernacexpr.Plus n -> Pp.(str (String.make n '+'))
+ | Dash n -> Pp.(str (String.make n '-'))
+ | Star n -> Pp.(str (String.make n '*'))
+ | Plus n -> Pp.(str (String.make n '+'))
type behavior = {
@@ -195,54 +198,5 @@ let put p b =
let suggest p =
(!current_behavior).suggest p
-(**********************************************************)
-(* *)
-(* Default goal selector *)
-(* *)
-(**********************************************************)
-
-
-(* Default goal selector: selector chosen when a tactic is applied
- without an explicit selector. *)
-let default_goal_selector = ref (Vernacexpr.SelectNth 1)
-let get_default_goal_selector () = !default_goal_selector
-
-let pr_range_selector (i, j) =
- if i = j then Pp.int i
- else Pp.(int i ++ str "-" ++ int j)
-
-let pr_goal_selector = function
- | Vernacexpr.SelectAlreadyFocused -> Pp.str "!"
- | Vernacexpr.SelectAll -> Pp.str "all"
- | Vernacexpr.SelectNth i -> Pp.int i
- | Vernacexpr.SelectList l ->
- Pp.(str "["
- ++ prlist_with_sep pr_comma pr_range_selector l
- ++ str "]")
- | Vernacexpr.SelectId id -> Names.Id.print id
-
-let parse_goal_selector = function
- | "!" -> Vernacexpr.SelectAlreadyFocused
- | "all" -> Vernacexpr.SelectAll
- | i ->
- let err_msg = "The default selector must be \"all\" or \"!\" or a natural number." in
- begin try
- let i = int_of_string i in
- if i < 0 then CErrors.user_err Pp.(str err_msg);
- Vernacexpr.SelectNth i
- with Failure _ -> CErrors.user_err Pp.(str err_msg)
- end
-
-let _ =
- Goptions.(declare_string_option{optdepr = false;
- optname = "default goal selector" ;
- optkey = ["Default";"Goal";"Selector"] ;
- optread = begin fun () ->
- Pp.string_of_ppcmds
- (pr_goal_selector !default_goal_selector)
- end;
- optwrite = begin fun n ->
- default_goal_selector := parse_goal_selector n
- end
- })
-
+let pr_goal_selector = Goal_select.pr_goal_selector
+let get_default_goal_selector = Goal_select.get_default_goal_selector
diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli
index ffbaa0fac..a09a7ec1d 100644
--- a/proofs/proof_bullet.mli
+++ b/proofs/proof_bullet.mli
@@ -14,7 +14,10 @@
(* *)
(**********************************************************)
-type t = Vernacexpr.bullet
+type t =
+ | Dash of int
+ | Star of int
+ | Plus of int
(** A [behavior] is the data of a put function which
is called when a bullet prefixes a tactic, a suggest function
@@ -42,12 +45,8 @@ val register_behavior : behavior -> unit
val put : Proof.t -> t -> Proof.t
val suggest : Proof.t -> Pp.t
-(**********************************************************)
-(* *)
-(* Default goal selector *)
-(* *)
-(**********************************************************)
-
-val pr_goal_selector : Vernacexpr.goal_selector -> Pp.t
-val get_default_goal_selector : unit -> Vernacexpr.goal_selector
-
+(** Deprecated *)
+val pr_goal_selector : Goal_select.t -> Pp.t
+[@@ocaml.deprecated "Please use [Goal_select.pr_goal_selector]"]
+val get_default_goal_selector : unit -> Goal_select.t
+[@@ocaml.deprecated "Please use [Goal_select.get_default_goal_selector]"]
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index fc7c437e6..842003bc8 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -83,6 +83,7 @@ type proof_ending =
| Proved of Vernacexpr.opacity_flag *
Misctypes.lident option *
proof_object
+
type proof_terminator = proof_ending -> unit
type closed_proof = proof_object * proof_terminator
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 058e839b4..197f71ca9 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -5,6 +5,7 @@ Proof_type
Logic
Refine
Proof
+Goal_select
Proof_bullet
Proof_global
Redexpr
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 0af766219..b8af2bcd5 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -23,8 +23,8 @@ val crawl :
static_block_declaration option
val unit_val : Stm.DynBlockData.t
-val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t
-val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet
+val of_bullet_val : Proof_bullet.t -> Stm.DynBlockData.t
+val to_bullet_val : Stm.DynBlockData.t -> Proof_bullet.t
val of_vernac_control_val : Vernacexpr.vernac_control -> Stm.DynBlockData.t
val to_vernac_control_val : Stm.DynBlockData.t -> Vernacexpr.vernac_control
diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli
index 9784de114..eacd3687a 100644
--- a/stm/proofBlockDelimiter.mli
+++ b/stm/proofBlockDelimiter.mli
@@ -38,6 +38,6 @@ val crawl :
val unit_val : Stm.DynBlockData.t
(* Bullets *)
-val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t
-val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet
+val of_bullet_val : Proof_bullet.t -> Stm.DynBlockData.t
+val to_bullet_val : Stm.DynBlockData.t -> Proof_bullet.t
diff --git a/stm/stm.ml b/stm/stm.ml
index cbd324f5c..9ea6a305e 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2288,7 +2288,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
Proof_global.unfreeze proof;
Proof_global.with_current_proof (fun _ p ->
feedback ~id:id Feedback.AddedAxiom;
- fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ());
+ fst (Pfedit.solve Goal_select.SelectAll None tac p), ());
(* STATE SPEC:
* - start: Modifies the input state adding a proof.
* - end : maybe after recovery command.
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 82b178388..6c7db26c7 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -492,12 +492,12 @@ module New = struct
Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t)
(* Select a subset of the goals *)
- let tclSELECT = function
- | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i
- | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l
- | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id
- | Vernacexpr.SelectAll -> anomaly ~label:"tclSELECT" Pp.(str "SelectAll not allowed here")
- | Vernacexpr.SelectAlreadyFocused ->
+ let tclSELECT = let open Goal_select in function
+ | SelectNth i -> Proofview.tclFOCUS i i
+ | SelectList l -> Proofview.tclFOCUSLIST l
+ | SelectId id -> Proofview.tclFOCUSID id
+ | SelectAll -> anomaly ~label:"tclSELECT" Pp.(str "SelectAll not allowed here")
+ | SelectAlreadyFocused ->
anomaly ~label:"tclSELECT" Pp.(str "SelectAlreadyFocused not allowed here")
(* Check that holes in arguments have been resolved *)
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 340d8fbf3..bc2f60186 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -223,7 +223,7 @@ module New : sig
val tclCOMPLETE : 'a tactic -> 'a tactic
val tclSOLVE : unit tactic list -> unit tactic
val tclPROGRESS : unit tactic -> unit tactic
- val tclSELECT : Vernacexpr.goal_selector -> 'a tactic -> 'a tactic
+ val tclSELECT : Goal_select.t -> 'a tactic -> 'a tactic
val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic
val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index f6539d80b..e5f22f25e 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -382,7 +382,7 @@ real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles)
.PHONY: real-all
real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff)
-.PHONE: real-all.timing.diff
+.PHONY: real-all.timing.diff
bytefiles: $(CMOFILES) $(CMAFILES)
.PHONY: bytefiles
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 668f9b893..e60382f2c 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -435,10 +435,22 @@ let init_toplevel arglist =
* early since the master waits us to connect back *)
Spawned.init_channels ();
Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
- if opts.print_where then (print_endline(Envars.coqlib ()); exit(exitcode opts));
- if opts.print_config then (Envars.print_config stdout Coq_config.all_src_dirs; exit (exitcode opts));
- if opts.print_tags then (print_style_tags opts; exit (exitcode opts));
- if opts.filter_opts then (print_string (String.concat "\n" extras); exit 0);
+ if opts.print_where then begin
+ print_endline (Envars.coqlib ());
+ exit (exitcode opts)
+ end;
+ if opts.print_config then begin
+ Envars.print_config stdout Coq_config.all_src_dirs;
+ exit (exitcode opts)
+ end;
+ if opts.print_tags then begin
+ print_style_tags opts;
+ exit (exitcode opts)
+ end;
+ if opts.filter_opts then begin
+ print_string (String.concat "\n" extras);
+ exit 0;
+ end;
let top_lp = Coqinit.toplevel_init_load_path () in
List.iter Mltop.add_coq_path top_lp;
Option.iter Mltop.load_ml_object_raw opts.toploop;
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 564c0965b..f0e41d27c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -909,7 +909,7 @@ let vernac_set_used_variables e =
if List.is_empty to_clear then (p, ())
else
let tac = Tactics.clear to_clear in
- fst (Pfedit.solve SelectAll None tac p), ()
+ fst (Pfedit.solve Goal_select.SelectAll None tac p), ()
end
(*****************************)
@@ -1611,7 +1611,7 @@ let get_current_context_of_args = function
let query_command_selector ?loc = function
| None -> None
- | Some (SelectNth n) -> Some n
+ | Some (Goal_select.SelectNth n) -> Some n
| _ -> user_err ?loc ~hdr:"query_command_selector"
(str "Query commands only support the single numbered goal selector.")
@@ -1911,7 +1911,7 @@ let vernac_subproof gln =
Proof_global.simple_with_current_proof (fun _ p ->
match gln with
| None -> Proof.focus subproof_cond () 1 p
- | Some (SelectNth n) -> Proof.focus subproof_cond () n p
+ | Some (Goal_select.SelectNth n) -> Proof.focus subproof_cond () n p
| _ -> user_err ~hdr:"bracket_selector"
(str "Brackets only support the single numbered goal selector."))
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 01:18:05 +0000