aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Collapse)Author
2021-03-06Merge PR #13882: Fix #12011 ssreflect "rewrite in" with setoidsPierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot
2021-03-05Merge PR #13842: Remove decimal-only number notations (deprecated in 8.12)Pierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2021-03-04Fix #12011 ssreflect "rewrite in" with setoidsGaëtan Gilbert
ssreflect asks setoid rewrite to rewrite in goal "forall_special_name_ : T, _other_name_" Since this is a non dependent product, setoid rewrite converts that to "impl T _other_name_" and must be taught to restore the special name when unfolding impl.
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
We introduce a new package structure for Coq: - `coq-core`: Coq's OCaml tools code and plugins - `coq-stdlib`: Coq's stdlib [.vo files] - `coq`: meta-package that pulls `coq-{core,stdlib}` This has several advantages, in particular it allows to install Coq without the stdlib which is useful in several scenarios, it also open the door towards a versioning of the stdlib at the package level. The main user-visible change is that Coq's ML development files now live in `$lib/coq-core`, for compatibility in the regular build we install a symlink and support both setups for a while. Note that plugin developers and even `coq_makefile` should actually rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust. There is a transient state where we actually look for both `$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support the non-ocamlfind plus custom variables. This will be much improved once #13617 is merged (which requires this PR first), then, we will introduce a `coq.boot` library so finally `coqdep`, `coqchk`, etc... can share the same path setup code. IMHO the plan should work fine.
2021-02-27Remove decimal-only number notationsPierre Roux
This was deprecated in 8.12
2021-02-26Signed primitive integersAna
Signed primitive integers defined on top of the existing unsigned ones with two's complement. The module Sint63 includes the theory of signed primitive integers that differs from the unsigned case. Additions to the kernel: les (signed <=), lts (signed <), compares (signed compare), divs (signed division), rems (signed remainder), asr (arithmetic shift right) (The s suffix is not used when importing the Sint63 module.) The printing and parsing of primitive ints was updated and the int63_syntax_plugin was removed (we use Number Notation instead). A primitive int is parsed / printed as unsigned or signed depending on the scope. In the default (Set Printing All) case, it is printed in hexadecimal.
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-02-10[micromega/nia] Improve sharing of proofsBESSON Frederic
Closes #13794
2021-02-03Fix #13739 - disable some warnings when calling Function.Pierre Courtieu
Also added a generic way of temporarily disabling a warning. Also added try_finalize un lib/utils.ml.
2021-01-28Merge PR #13781: [micromega] Deprecate hopefully useless options and flagscoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: jfehrle
2021-01-28Merge PR #13790: [vernac] Check that no proofs do remain open at ↵coqbot-app[bot]
section/module closing time Reviewed-by: SkySkimmer
2021-01-27[ltac] break dependency on the STMEnrico Tassi
2021-01-26[vernac] Check that no proofs do remain open at section/module closing timeEmilio Jesus Gallego Arias
Fixes #13755 .
2021-01-24Merge PR #13762: Remove double induction tacticPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2021-01-22[micromega] Deprecate hopefully useless options and flagsBESSON Frederic
The goal is to eventually only use the Simplex solver and remove all the code needed for fourier elimination.
2021-01-22Merge PR #13761: Remove convert_concl_no_check (deprecated in 8.11)Pierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2021-01-20Remove double induction tacticJim Fehrle
2021-01-19Remove Add InjTyp and 10 other micromega commandsJim Fehrle
2021-01-19Remove convert_concl_no_checkJim Fehrle
2021-01-19Merge PR #13725: Support locality attributes for Hint Rewrite (including export)Pierre-Marie Pédrot
Ack-by: Zimmi48 Ack-by: gares Reviewed-by: ppedrot
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
We deprecate unspecified locality as was done for Hint. Close #13724
2021-01-13Avoid using "subgoals" in the UI, it means the same as "goals"Jim Fehrle
2021-01-10Merge PR #13469: Use nat_or_var for fail/gfailPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2021-01-09Merge PR #13299: Remember universe instances of constants in notationscoqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: herbelin
2021-01-07Use nat_or_var for fail/gfailJim Fehrle
2021-01-07Merge PR #13696: Deprecate "at ... with ..." in change tactic (use "with ... ↵Pierre-Marie Pédrot
at ..." instead) Ack-by: Zimmi48 Reviewed-by: ppedrot
2021-01-07Merge PR #13715: [micromega] Add missing support for `implb`Vincent Laporte
Reviewed-by: vbgl
2021-01-06[micromega] Add missing support for `implb`BESSON Frederic
2021-01-04Remember universe instances of constants in notationsJasper Hugunin
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
We store bound variable names instead of functions for both branches and predicate, and we furthermore add the parameters in the node. Let bindings are not taken into account and require an environment lookup for retrieval.
2021-01-02Deprecate "at ... with ..." in change tacticJim Fehrle
(use "with ... at ..." instead)
2020-12-30Merge PR #13321: Move evaluable_global_reference from Names to Tacred.coqbot-app[bot]
Reviewed-by: herbelin Ack-by: ejgallego
2020-12-27Merge PR #13659: Make ssr datastructures cpattern and rpattern publiccoqbot-app[bot]
Reviewed-by: gares
2020-12-27Refactor cpattern into a recordLasse Blaauwbroek
2020-12-27Make ssrtermkind algebraic instead of a charLasse Blaauwbroek
2020-12-21Move evaluable_global_reference from Names to Tacred.Pierre-Marie Pédrot
It is the only place where it starts making sense in the whole codebase. It also fits nicely there since there are other functions manipulating this type in that module. In any case this type does not belong to the kernel.
2020-12-18Merge PR #13530: Revert removal of eoi_entry in #13447coqbot-app[bot]
Reviewed-by: herbelin
2020-12-18Make ssr datastructures cpattern and rpattern publicLasse Blaauwbroek
2020-12-14Add checks for invalid occurrences in setoid rewrite.Hugo Herbelin
We additionally check that occurrence 0 is invalid in simpl at, unfold at, etc.
2020-12-11Revert removal of eoi_entry in #13447Jim Fehrle
2020-12-11Use a registered printer for tactic coercion failure.Pierre-Marie Pédrot
Otherwise we pay a high cost for printing that might never make it to the user.
2020-12-08Congruence: don't replace error messages by "congruence failed"Gaëtan Gilbert
Fix #13595
2020-12-08Reindent Cctac.cc_tacticGaëtan Gilbert
2020-12-02Merge PR #13275: Put all Int63 primitives in a separate fileVincent Laporte
Ack-by: SkySkimmer Ack-by: ppedrot Reviewed-by: vbgl
2020-12-02Put all Int63 primitives in a separate filePierre Roux
Following a request from Pierre-Marie Pédrot in #13258
2020-12-01Fix a bug in funind.Pierre-Marie Pédrot
It was generating a completely nonsense case branch, but for some reason the proof still went trough.
2020-11-29Merge PR #13510: Add missing print registration for wit_nat_or_varcoqbot-app[bot]
Reviewed-by: herbelin
2020-11-29Fixing printing of apply in (continuation of #12246).Hugo Herbelin
2020-11-28Add missing print registration for wit_nat_or_varJim Fehrle
2020-11-27Revert "Remove deprecated tactic cutrewrite."Théo Zimmermann
This reverts commit f3642ad8bdf6d9aa1b411892e5e6815a6a75e4d5.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 00:47:33 +0000