diff options
| -rw-r--r-- | .gitlab-ci.yml | 10 | ||||
| -rw-r--r-- | CONTRIBUTING.md | 6 | ||||
| -rwxr-xr-x | dev/lint-commits.sh | 31 | ||||
| -rw-r--r-- | doc/changelog/04-tactics/10318-select-only-error.rst | 4 | ||||
| -rw-r--r-- | doc/changelog/08-tools/10245-require-command-line.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 25 | ||||
| -rw-r--r-- | engine/proofview.ml | 42 | ||||
| -rw-r--r-- | proofs/refine.ml | 3 | ||||
| -rw-r--r-- | proofs/refine.mli | 3 | ||||
| -rw-r--r-- | proofs/refiner.ml | 55 | ||||
| -rw-r--r-- | proofs/refiner.mli | 29 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 9 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 4 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 8 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 9 | ||||
| -rw-r--r-- | test-suite/success/goal_selector.v | 8 | ||||
| -rw-r--r-- | toplevel/coqargs.ml | 21 | ||||
| -rw-r--r-- | toplevel/usage.ml | 17 |
18 files changed, 117 insertions, 173 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 1be10f91d0..8cf26ffaa6 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -295,16 +295,12 @@ windows32: - /^pr-.*$/ lint: - image: docker:git stage: test - script: - - apk add bash - - dev/lint-repository.sh + script: dev/lint-repository.sh dependencies: [] - before_script: [] variables: - # we need an unknown amount of history for per-commit linting - GIT_DEPTH: "" + GIT_DEPTH: "" # we need an unknown amount of history for per-commit linting + OPAM_SWITCH: base pkg:opam: stage: test diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index f0e17909c1..0d11d092ba 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -105,6 +105,12 @@ files end with newlines) is checked by the `lint` job on GitLab CI (using git hook which fixes these errors at commit time. `configure` automatically sets you up to use it, unless you already have a hook at `.git/hooks/pre-commit`. +Each commit in your pull request should compile (this makes bisecting +easier). The `lint` job checks compilation of the OCaml files, please +try to keep the rest of Coq in a functioning state as well. + +You may run the linter yourself with `dev/lint-repository.sh`. + Here are a few tags Coq developers may add to your PR and what they mean. In general feedback and requests for you as the pull request author will be in the comments and tags are only used to organize pull requests. diff --git a/dev/lint-commits.sh b/dev/lint-commits.sh index 96c92e3162..539bb5f1f9 100755 --- a/dev/lint-commits.sh +++ b/dev/lint-commits.sh @@ -19,21 +19,40 @@ fi BASE_COMMIT="$1" HEAD_COMMIT="$2" -bad=() +bad_ws=() +bad_compile=() while IFS= read -r commit; do echo Checking "$commit" # git diff --check # uses .gitattributes to know what to check if ! git diff --check "${commit}^" "$commit"; - then - bad+=("$commit") + then bad_ws+=("$commit") + fi + + if ! make -f Makefile.dune check + then bad_compile+=("$commit") fi done < <(git rev-list "$HEAD_COMMIT" --not "$BASE_COMMIT" --) -if [ "${#bad[@]}" != 0 ] +# report errors + +CODE=0 + +if [ "${#bad_ws[@]}" != 0 ] then >&2 echo "Whitespace errors!" - >&2 echo "In commits ${bad[*]}" + >&2 echo "In commits ${bad_ws[*]}" >&2 echo "If you use emacs, you can prevent this kind of error from reoccurring by installing ws-butler and enabling ws-butler-convert-leading-tabs-or-spaces." - exit 1 + >&2 echo + CODE=1 fi + +if [ "${#bad_compile[@]}" != 0 ] +then + >&2 echo "Compilation errors!" + >&2 echo "In commits ${bad_compile[*]}" + >&2 echo + CODE=1 +fi + +exit $CODE diff --git a/doc/changelog/04-tactics/10318-select-only-error.rst b/doc/changelog/04-tactics/10318-select-only-error.rst new file mode 100644 index 0000000000..03ed15d948 --- /dev/null +++ b/doc/changelog/04-tactics/10318-select-only-error.rst @@ -0,0 +1,4 @@ +- The goal selector tactical ``only`` now checks that the goal range + it is given is valid instead of ignoring goals out of the focus + range. (`#10318 <https://github.com/coq/coq/pull/10318>`_, by Gaëtan + Gilbert). diff --git a/doc/changelog/08-tools/10245-require-command-line.rst b/doc/changelog/08-tools/10245-require-command-line.rst new file mode 100644 index 0000000000..54417077f5 --- /dev/null +++ b/doc/changelog/08-tools/10245-require-command-line.rst @@ -0,0 +1,6 @@ +- Add command line options `-require-import`, `-require-export`, + `-require-import-from` and `-require-export-from`, as well as their + shorthand, `-ri`, `-re`, `-refrom` and -`rifrom`. Deprecate + confusing command line option `-require` + (`#10245 <https://github.com/coq/coq/pull/10245>`_ + by Hugo Herbelin, review by Emilio Gallego). diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index bdda35fcc0..48d5f4075e 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -124,11 +124,11 @@ and ``coqtop``, unless stated otherwise: :ref:`names-of-libraries` and the command Declare ML Module Section :ref:`compiled-files`. -:-Q *directory* dirpath: Add physical path *directory* to the list of +:-Q *directory* *dirpath*: Add physical path *directory* to the list of directories where |Coq| looks for a file and bind it to the logical directory *dirpath*. The subdirectory structure of *directory* is recursively available from |Coq| using absolute names (extending the - dirpath prefix) (see Section :ref:`qualified-names`).Note that only those + :n:`@dirpath` prefix) (see Section :ref:`qualified-names`). Note that only those subdirectories and files which obey the lexical conventions of what is an :n:`@ident` are taken into account. Conversely, the underlying file systems or operating systems may be more restrictive @@ -138,13 +138,13 @@ and ``coqtop``, unless stated otherwise: disallow two files differing only in the case in the same directory. .. seealso:: Section :ref:`names-of-libraries`. -:-R *directory* dirpath: Do as -Q *directory* dirpath but make the +:-R *directory* *dirpath*: Do as ``-Q`` *directory* *dirpath* but make the subdirectory structure of *directory* recursively visible so that the recursive contents of physical *directory* is available from |Coq| using short or partially qualified names. .. seealso:: Section :ref:`names-of-libraries`. -:-top dirpath: Set the toplevel module name to dirpath instead of Top. +:-top *dirpath*: Set the toplevel module name to :n:`@dirpath` instead of ``Top``. Not valid for `coqc` as the toplevel module name is inferred from the name of the output file. :-exclude-dir *directory*: Exclude any subdirectory named *directory* @@ -164,10 +164,17 @@ and ``coqtop``, unless stated otherwise: :-lv *file*, -load-vernac-source-verbose *file*: Load and execute the |Coq| script from *file.v*. Write its contents to the standard output as it is executed. -:-load-vernac-object dirpath: Load |Coq| compiled library dirpath. This - is equivalent to runningRequire dirpath. -:-require dirpath: Load |Coq| compiled library dirpath and import it. - This is equivalent to running Require Import dirpath. +:-load-vernac-object *qualid*: Load |Coq| compiled library :n:`@qualid`. This + is equivalent to running :cmd:`Require` :n:`qualid`. +:-ri *qualid*, -require-import *qualid*: Load |Coq| compiled library :n:`@qualid` and import it. + This is equivalent to running :cmd:`Require Import` :n:`@qualid`. +:-re *qualid*, -require-export *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it. + This is equivalent to running :cmd:`Require Export` :n:`@qualid`. +:-rifrom *dirpath* *qualid*, -require-import-from *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid` and import it. + This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Import` :n:`@qualid`. +:-refrom *dirpath* *qualid*, -require-export-from *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it. + This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Export` :n:`@qualid`. +:-require *qualid*: Deprecated; use ``-ri`` *qualid*. :-batch: Exit just after argument parsing. Available for ``coqtop`` only. :-compile *file.v*: Deprecated; use ``coqc`` instead. Compile file *file.v* into *file.vo*. This option implies -batch (exit just after argument parsing). It is available only @@ -193,7 +200,7 @@ and ``coqtop``, unless stated otherwise: :-emacs, -ide-slave: Start a special toplevel to communicate with a specific IDE. :-impredicative-set: Change the logical theory of |Coq| by declaring the - sort Set impredicative. + sort :g:`Set` impredicative. .. warning:: diff --git a/engine/proofview.ml b/engine/proofview.ml index c00c90e5e9..d4f6fe3aef 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -373,32 +373,24 @@ let tclTRYFOCUS i j t = tclFOCUS ~nosuchgoal:(tclUNIT ()) i j t let tclFOCUSLIST ?(nosuchgoal=tclZERO (NoSuchGoals 0)) l t = let open Proof in Comb.get >>= fun comb -> - let n = CList.length comb in - (* First, remove empty intervals, and bound the intervals to the number - of goals. *) - let sanitize (i, j) = - if i > j then None - else if i > n then None - else if j < 1 then None - else Some ((max i 1), (min j n)) - in - let l = CList.map_filter sanitize l in + let n = CList.length comb in + let ok (i, j) = 1 <= i && i <= j && j <= n in + if not (CList.for_all ok l) then nosuchgoal + else match l with - | [] -> nosuchgoal - | (mi, _) :: _ -> - (* Get the left-most goal to focus. This goal won't move, and we - will then place all the other goals to focus to the right. *) - let mi = CList.fold_left (fun m (i, _) -> min m i) mi l in - (* [CList.goto] returns a zipper, so that - [(rev left) @ sub_right = comb]. *) - let left, sub_right = CList.goto (mi-1) comb in - let p x _ = CList.exists (fun (i, j) -> i <= x + mi && x + mi <= j) l in - let sub, right = CList.partitioni p sub_right in - let mj = mi - 1 + CList.length sub in - Comb.set (CList.rev_append left (sub @ right)) >> - tclFOCUS mi mj t - - + | [] -> nosuchgoal + | (mi, _) :: _ -> + (* Get the left-most goal to focus. This goal won't move, and we + will then place all the other goals to focus to the right. *) + let mi = CList.fold_left (fun m (i, _) -> min m i) mi l in + (* [CList.goto] returns a zipper, so that + [(rev left) @ sub_right = comb]. *) + let left, sub_right = CList.goto (mi-1) comb in + let p x _ = CList.exists (fun (i, j) -> i <= x + mi && x + mi <= j) l in + let sub, right = CList.partitioni p sub_right in + let mj = mi - 1 + CList.length sub in + Comb.set (CList.rev_append left (sub @ right)) >> + tclFOCUS mi mj t (** Like {!tclFOCUS} but selects a single goal by name. *) let tclFOCUSID ?(nosuchgoal=tclZERO (NoSuchGoals 1)) id t = diff --git a/proofs/refine.ml b/proofs/refine.ml index 4a9404aa96..8439156e65 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -116,9 +116,6 @@ let lift c = let make_refine_enter ~typecheck f gl = generic_refine ~typecheck (lift f) gl -let refine_one ~typecheck f = - Proofview.Goal.enter_one (make_refine_enter ~typecheck f) - let refine ~typecheck f = let f evd = let (evd,c) = f evd in (evd,((), c)) diff --git a/proofs/refine.mli b/proofs/refine.mli index b8948a92f3..93fd9d7a64 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -27,9 +27,6 @@ val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> uni raised during the interpretation of [t] are caught and result in tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *) -val refine_one : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr.t)) -> 'a tactic -(** A variant of [refine] which assumes exactly one goal under focus *) - val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic -> Proofview.Goal.t -> 'a tactic (** The general version of refine. *) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 799f4a380b..557f428be9 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -129,9 +129,6 @@ let tclTHENSLASTn tac1 tac taci = tclTHENS3PARTS tac1 [||] tac taci let tclTHEN_i tac taci gls = finish_tac (thensi_tac taci (then_tac tac (start_tac gls))) -let tclTHENLASTn tac1 taci = tclTHENSLASTn tac1 tclIDTAC taci -let tclTHENFIRSTn tac1 taci = tclTHENSFIRSTn tac1 taci tclIDTAC - (* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies [tac2] to every resulting subgoals *) let tclTHEN tac1 tac2 = tclTHENS3PARTS tac1 [||] tac2 [||] @@ -253,46 +250,9 @@ let rec tclFIRST = function | [] -> tclFAIL_s "No applicable tactic." | t::rest -> tclORELSE0 t (tclFIRST rest) -let ite_gen tcal tac_if continue tac_else gl= - let success=ref false in - let tac_if0 gl= - let result=tac_if gl in - success:=true;result in - let tac_else0 e gl= - if !success then - iraise e - else - try - tac_else gl - with - e' when CErrors.noncritical e' -> iraise e in - try - tcal tac_if0 continue gl - with (* Breakpoint *) - | e when CErrors.noncritical e -> - let e = CErrors.push e in catch_failerror e; tac_else0 e gl - -(* Try the first tactic and, if it succeeds, continue with - the second one, and if it fails, use the third one *) - -let tclIFTHENELSE=ite_gen tclTHEN - -(* Idem with tclTHENS and tclTHENSV *) - -let tclIFTHENSELSE=ite_gen tclTHENS - -let tclIFTHENSVELSE=ite_gen tclTHENSV - -let tclIFTHENTRYELSEMUST tac1 tac2 gl = - tclIFTHENELSE tac1 (tclTRY tac2) tac2 gl - (* Fails if a tactic did not solve the goal *) let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.") -(* Try the first that solves the current goal *) -let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl) - - (* Iteration tacticals *) let tclDO n t = @@ -311,22 +271,7 @@ let rec tclREPEAT t g = let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t)) -(* Repeat on the first subgoal (no failure if no more subgoal) *) -let rec tclREPEAT_MAIN t g = - (tclORELSE (tclTHEN_i t (fun i -> if Int.equal i 1 then (tclREPEAT_MAIN t) else - tclIDTAC)) tclIDTAC) g - (* Change evars *) let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} - -let tclEVARUNIVCONTEXT ctx gls = tclIDTAC {gls with sigma= Evd.set_universe_context gls.sigma ctx} - -(* Push universe context *) -let tclPUSHCONTEXT rigid ctx tac gl = - tclTHEN (tclEVARS (Evd.merge_context_set rigid (project gl) ctx)) tac gl - let tclPUSHEVARUNIVCONTEXT ctx gl = tclEVARS (Evd.merge_universe_context (project gl) ctx) gl - -let tclPUSHCONSTRAINTS cst gl = - tclEVARS (Evd.add_constraints (project gl) cst) gl diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 52cbf7658b..0f34a79c49 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -32,12 +32,8 @@ val tclIDTAC_MESSAGE : Pp.t -> tactic (** [tclEVARS sigma] changes the current evar map *) val tclEVARS : evar_map -> tactic -val tclEVARUNIVCONTEXT : UState.t -> tactic - -val tclPUSHCONTEXT : Evd.rigid -> Univ.ContextSet.t -> tactic -> tactic val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic -val tclPUSHCONSTRAINTS : Univ.Constraint.t -> tactic (** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies [tac2] to every resulting subgoals *) @@ -86,16 +82,6 @@ val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic [tac2] for the remaining last subgoals (previously called tclTHENST) *) val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic -(** [tclTHENLASTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then, - applies [t1],...,[tn] on the last [n] resulting subgoals and leaves - unchanged the other subgoals *) -val tclTHENLASTn : tactic -> tactic array -> tactic - -(** [tclTHENFIRSTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then, - applies [t1],...,[tn] on the first [n] resulting subgoals and leaves - unchanged the other subgoals (previously called [tclTHENSI]) *) -val tclTHENFIRSTn : tactic -> tactic array -> tactic - (** A special exception for levels for the Fail tactic *) exception FailError of int * Pp.t Lazy.t @@ -106,9 +92,7 @@ val catch_failerror : Exninfo.iexn -> unit val tclORELSE0 : tactic -> tactic -> tactic val tclORELSE : tactic -> tactic -> tactic val tclREPEAT : tactic -> tactic -val tclREPEAT_MAIN : tactic -> tactic val tclFIRST : tactic list -> tactic -val tclSOLVE : tactic list -> tactic val tclTRY : tactic -> tactic val tclTHENTRY : tactic -> tactic -> tactic val tclCOMPLETE : tactic -> tactic @@ -118,16 +102,3 @@ val tclFAIL_lazy : int -> Pp.t Lazy.t -> tactic val tclDO : int -> tactic -> tactic val tclPROGRESS : tactic -> tactic val tclSHOWHYPS : tactic -> tactic - -(** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then, - if it succeeds, applies [tac2] to the resulting subgoals, - and if not applies [tac3] to the initial goal [gls] *) -val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic -val tclIFTHENSELSE : tactic -> tactic list -> tactic ->tactic -val tclIFTHENSVELSE : tactic -> tactic array -> tactic ->tactic - -(** [tclIFTHENTRYELSEMUST tac1 tac2 gls] applies [tac1] then [tac2]. If [tac1] - has been successful, then [tac2] may fail. Otherwise, [tac2] must succeed. - Equivalent to [(tac1;try tac2)||tac2] *) - -val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 93031c2202..d7b4f729cb 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -81,12 +81,10 @@ let pf_type_of = pf_reduce type_of let pf_get_type_of = pf_reduce Retyping.get_type_of let pf_conv_x gl = pf_reduce test_conversion gl Reduction.CONV -let pf_conv_x_leq gl = pf_reduce test_conversion gl Reduction.CUMUL let pf_const_value = pf_reduce (fun env _ c -> EConstr.of_constr (constant_value_in env c)) let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind - let pf_hnf_type_of gls = pf_get_type_of gls %> pf_whd_all gls (* Pretty-printers *) @@ -181,14 +179,7 @@ module New = struct let pf_hnf_type_of gl t = pf_whd_all gl (pf_get_type_of gl t) - let pf_whd_all gl t = pf_apply whd_all gl t let pf_compute gl t = pf_apply compute gl t let pf_nf_evar gl t = nf_evar (project gl) t - - let pf_undefined_evars gl = - let sigma = Proofview.Goal.sigma gl in - let ev = Proofview.Goal.goal gl in - let evi = Evd.find sigma ev in - Evarutil.filtered_undefined_evars_of_evar_info sigma evi end diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 23e1e6f566..195be04986 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -64,7 +64,6 @@ val pf_unfoldn : (occurrences * evaluable_global_reference) list val pf_const_value : Goal.goal sigma -> pconstant -> constr val pf_conv_x : Goal.goal sigma -> constr -> constr -> bool -val pf_conv_x_leq : Goal.goal sigma -> constr -> constr -> bool (** {6 Pretty-printing functions (debug only). } *) val pr_gls : Goal.goal sigma -> Pp.t @@ -109,11 +108,8 @@ module New : sig val pf_hnf_constr : Proofview.Goal.t -> constr -> types val pf_hnf_type_of : Proofview.Goal.t -> constr -> types - val pf_whd_all : Proofview.Goal.t -> constr -> constr val pf_compute : Proofview.Goal.t -> constr -> constr val pf_nf_evar : Proofview.Goal.t -> constr -> constr - (** Gathers the undefined evars of the given goal. *) - val pf_undefined_evars : Proofview.Goal.t -> Evar.Set.t end diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 59fd8b37d6..81700986ea 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -43,12 +43,8 @@ let tclTHENS = Refiner.tclTHENS let tclTHENSV = Refiner.tclTHENSV let tclTHENSFIRSTn = Refiner.tclTHENSFIRSTn let tclTHENSLASTn = Refiner.tclTHENSLASTn -let tclTHENFIRSTn = Refiner.tclTHENFIRSTn -let tclTHENLASTn = Refiner.tclTHENLASTn let tclREPEAT = Refiner.tclREPEAT -let tclREPEAT_MAIN = Refiner.tclREPEAT_MAIN let tclFIRST = Refiner.tclFIRST -let tclSOLVE = Refiner.tclSOLVE let tclTRY = Refiner.tclTRY let tclCOMPLETE = Refiner.tclCOMPLETE let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE @@ -58,10 +54,6 @@ let tclDO = Refiner.tclDO let tclPROGRESS = Refiner.tclPROGRESS let tclSHOWHYPS = Refiner.tclSHOWHYPS let tclTHENTRY = Refiner.tclTHENTRY -let tclIFTHENELSE = Refiner.tclIFTHENELSE -let tclIFTHENSELSE = Refiner.tclIFTHENSELSE -let tclIFTHENSVELSE = Refiner.tclIFTHENSVELSE -let tclIFTHENTRYELSEMUST = Refiner.tclIFTHENTRYELSEMUST (************************************************************************) (* Tacticals applying on hypotheses *) diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 201b7801c3..a9ccda527f 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -31,13 +31,9 @@ val tclTHENLAST : tactic -> tactic -> tactic val tclTHENS : tactic -> tactic list -> tactic val tclTHENSV : tactic -> tactic array -> tactic val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic -val tclTHENLASTn : tactic -> tactic array -> tactic val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic -val tclTHENFIRSTn : tactic -> tactic array -> tactic val tclREPEAT : tactic -> tactic -val tclREPEAT_MAIN : tactic -> tactic val tclFIRST : tactic list -> tactic -val tclSOLVE : tactic list -> tactic val tclTRY : tactic -> tactic val tclCOMPLETE : tactic -> tactic val tclAT_LEAST_ONCE : tactic -> tactic @@ -49,11 +45,6 @@ val tclSHOWHYPS : tactic -> tactic val tclTHENTRY : tactic -> tactic -> tactic val tclMAP : ('a -> tactic) -> 'a list -> tactic -val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic -val tclIFTHENSELSE : tactic -> tactic list -> tactic -> tactic -val tclIFTHENSVELSE : tactic -> tactic array -> tactic -> tactic -val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic - (** {6 Tacticals applying to hypotheses } *) val onNthHypId : int -> (Id.t -> tactic) -> tactic diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v index 0951c5c8d4..ae834e7696 100644 --- a/test-suite/success/goal_selector.v +++ b/test-suite/success/goal_selector.v @@ -13,13 +13,15 @@ Goal two false /\ two true /\ two false /\ two true /\ two true /\ two true. Proof. do 2 dup. - repeat split. - 2, 4-99, 100-3:idtac. + Fail 7:idtac. + Fail 2-1:idtac. + 1,2,4-6:idtac. 2-5:exact One. par:exact Zero. - repeat split. 3-6:swap 1 4. 1-5:swap 1 5. - 0-4:exact One. + 1-4:exact One. all:exact Zero. - repeat split. 1, 3:exact Zero. @@ -34,7 +36,7 @@ Qed. Goal True -> True. Proof. - intros y; only 1-2 : repeat idtac. + intros y. 1-1:match goal with y : _ |- _ => let x := y in idtac x end. Fail 1-1:let x := y in idtac x. 1:let x := y in idtac x. diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 4ef31c73b7..9180cae389 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -184,6 +184,10 @@ let warn_deprecated_inputstate = CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.") +let warn_deprecated_simple_require = + CWarnings.create ~name:"deprecated-boot" ~category:"deprecated" + (fun () -> Pp.strbrk "The -require option is deprecated, please use -require-import instead.") + let set_inputstate opts s = warn_deprecated_inputstate (); { opts with inputstate = Some s } @@ -416,7 +420,22 @@ let parse_args ~help ~init arglist : t * string list = Flags.profile_ltac_cutoff := get_float opt (next ()); oval - |"-require" -> add_vo_require oval (next ()) None (Some false) + |"-rfrom" -> + let from = next () in add_vo_require oval (next ()) (Some from) None + + |"-require" -> + warn_deprecated_simple_require (); + add_vo_require oval (next ()) None (Some false) + + |"-require-import" | "-ri" -> add_vo_require oval (next ()) None (Some false) + + |"-require-export" | "-re" -> add_vo_require oval (next ()) None (Some true) + + |"-require-import-from" | "-rifrom" -> + let from = next () in add_vo_require oval (next ()) (Some from) (Some false) + + |"-require-export-from" | "-refrom" -> + let from = next () in add_vo_require oval (next ()) (Some from) (Some true) |"-top" -> let topname = Libnames.dirpath_of_string (next ()) in diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 29948d50b2..84d3992f5c 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -44,10 +44,23 @@ let print_usage_common co command = \n -load-ml-source f load ML file f\ \n -load-vernac-source f load Coq file f.v (Load \"f\".)\ \n -l f (idem)\ -\n -require path load Coq library path and import it (Require Import path.)\ \n -load-vernac-source-verbose f load Coq file f.v (Load Verbose \"f\".)\ \n -lv f (idem)\ -\n -load-vernac-object path load Coq library path (Require path)\ +\n -load-vernac-object lib, -r lib\ +\n load Coq library lib (Require lib)\ +\n -rfrom root lib load Coq library lib (From root Require lib.)\ +\n -require-import lib, -ri lib\ +\n load and import Coq library lib\ +\n (equivalent to Require Import lib.)\ +\n -require-export lib, -re lib\ +\n load and transitively import Coq library lib\ +\n (equivalent to Require Export lib.)\ +\n -require-import-from root lib, -rifrom lib\ +\n load and import Coq library lib\ +\n (equivalent to From root Require Import lib.)\ +\n -require-export-from root lib, -refrom lib\ +\n load and transitively import Coq library lib\ +\n (equivalent to From root Require Export lib.)\ \n\ \n -where print Coq's standard library location and exit\ \n -config, --config print Coq's configuration information and exit\ |