aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Collapse)Author
2020-09-22Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.Hugo Herbelin
2020-09-18Merge PR #12963: Formally deprecate the double induction tactic.Hugo Herbelin
Reviewed-by: VincentSe Ack-by: herbelin Ack-by: olaure01
2020-09-18Merge PR #12610: [leminv] [declare] Use higher-level Declare API.Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-09-17[leminv] Use higher-level Declare API.Emilio Jesus Gallego Arias
2020-09-17[leminv] Remove unused catch.Emilio Jesus Gallego Arias
2020-09-17[build] Don't link `num` anymore in CoqEmilio Jesus Gallego Arias
After #8743 we don't depend on `num` anymore in the codebase; thus we drop the dependency. This could create problems for plugins relying on this implicit linking.
2020-09-17Formally deprecate the double induction tactic.Pierre-Marie Pédrot
The doc states it is deprecated since 1386cd9 but this was ages before the deprecation mechanism existed.
2020-09-15[micromega] Use `minus_one` built-in zarith constant.Emilio Jesus Gallego Arias
2020-09-15[zarith] [micromega] Bump to 1.10 and remove some hacksEmilio Jesus Gallego Arias
In particular, behavior of `Z.gcd` and `Z.lcm` has been fixed in 1.10, see https://github.com/ocaml/Zarith/issues/58
2020-09-15[micromega] Migrate from num to zarithEmilio Jesus Gallego Arias
We still link num in `coqc` , that will be removed in a separate step. Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
2020-09-15[micromega] call csdpcert using path.Emilio Jesus Gallego Arias
2020-09-15Merge PR #13016: Remove deprecated Extraction Language command value "Ocaml"Pierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: pi8027 Reviewed-by: ppedrot
2020-09-14Remove deprecated Extraction Language command value "Ocaml"Jim Fehrle
2020-09-14[ocamlformat] Update to ocamlformat 0.15.0Emilio Jesus Gallego Arias
This is necessary to support OCaml 4.11 in development.
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
Keep Numeral Notation wit a deprecation warning.
2020-09-11Adding a wit_natural standard argument.Hugo Herbelin
2020-09-11Turn integer into natural in several mlgsPierre Roux
Negative values had no meaning there. Those were spotted by Hugo Herbelin while reviewing #12979 .
2020-09-11[refman] Rename int to integerPierre Roux
2020-09-11[parsing] Rename token NUMERAL to NUMBERPierre Roux
2020-09-08Merge PR #12993: Remove deprecated tactic cutrewrite.Clément Pit-Claudel
Reviewed-by: cpitclaudel Reviewed-by: ppedrot
2020-09-08Remove deprecated tactic cutrewrite.Théo Zimmermann
2020-09-06Fix printing of `change` tactic, which was printed as `change_no_check` and ↵Lasse Blaauwbroek
vice versa
2020-09-02Abstract type for allowed evarsMaxime Dénès
2020-09-02Replace `frozen` by `allowed` evars in evarconv, and delay themMaxime Dénès
This is a follow-up of #9062, which introduced a discrenpancy between the two unification engines.
2020-08-31Merge PR #12875: Further extensions of About wrt Arguments and renamingcoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: herbelin
2020-08-28Merge PR #12890: ring: generate fresh names for lemmascoqbot-app[bot]
Reviewed-by: herbelin Reviewed-by: maximedenes Ack-by: SkySkimmer
2020-08-28Merge PR #11742: [numeral] [plugins] Remove Coq's `Bigint` module in favor ↵coqbot-app[bot]
of ZArith. Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: liyishuai Ack-by: MSoegtropIMC Ack-by: ejgallego Ack-by: maximedenes Ack-by: proux01 Ack-by: vbgl
2020-08-28When reporting an implicit argument error on a rename argument, use the ↵Hugo Herbelin
renaming. Example: > Arguments id [B] {b} : rename. > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: Argument B is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ].
2020-08-27[nsatz] num → zarithVincent Laporte
2020-08-27[numeral] [plugins] Switch from `Big_int` to ZArith.Emilio Jesus Gallego Arias
We replace Coq's use of `Big_int` and `num` by the ZArith OCaml library which is a more modern version. We switch the core files and easy plugins only for now, more complex numerical plugins will be done in their own commit. We thus keep the num library linked for now until all plugins are ported. Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
2020-08-27Remove a call to the old refiner in ssr.Pierre-Marie Pédrot
2020-08-27tacinterp mini cleanup useless letinGaëtan Gilbert
2020-08-25omega: stop using intro_usingGaëtan Gilbert
This makes the test suite Omega.v compatible with Mangle Names Not sure how `reintroduce` works since it ignores the refreshed name, considering omega is deprecated it's not worth figuring out so long as it works (NB making it use intro_mustbe_force makes the test suite fail so it must be doing something right).
2020-08-25funind: stop using intro_usingGaëtan Gilbert
2020-08-25ring: generate fresh names for lemmasGaëtan Gilbert
Fix #12889
2020-08-23Merge PR #12851: Extraction: At declaration point of a global, use its ↵Maxime Dénès
declaring name Reviewed-by: maximedenes
2020-08-21Merge PR #12853: Another tactic error location fix after PR#12223 and PR#12774Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-08-20[ssr] when porting v8.2 code no backtracking point has to be addedEnrico Tassi
Amends c1b1afe76e1655cc3275bdf4215f0ab690efc3cc
2020-08-19Yet other tactic error location fixes (see PR#12223 and PR#12774).Hugo Herbelin
When calling an Ltac function, add specific locations when interpreting the function, when interpreting the arguments and when executating the call (in a TacArg).
2020-08-19Prefer eval_tactic_ist, which has error localisation, to interp_tactic.Hugo Herbelin
This is important for TacArg arguments, which typically corresponds to calling an Ltac function.
2020-08-19In tacinterp.ml, renaming eval_tactic into eval_tactic_ist to match the API.Hugo Herbelin
2020-08-19Merge PR #12725: Store evar identity instances in evarinfo / named_context_valEnrico Tassi
Ack-by: SkySkimmer Reviewed-by: gares
2020-08-18Extraction: At declaration point of a global, use its declaring name.Hugo Herbelin
If we need to print the name of an inlined constant (as in "let name =", "val name :" or "type name ="), we need its name without inlining nor qualification. In particular, we introduce a function pp_global_name to make it clearer that printing a name at declaration point of a global is only about printing the basename (formerly, Common.pp_global was correctly printing the basename without qualification thanks to the "top_visible_mp ()" test, but OCaml.pp_global was wrongly inlining).
2020-08-18Remaining bugs in PR#12223 which fixed location of tactic errors (issue #12152).Hugo Herbelin
The update of a loc needs sometimes to override (when calling an Ltac function), and otherwise to keep the existing loc (assumed to be fined). We refine this (see e.g. the ErrorLocation_tac_in_term tests). Moreover, when overriding, this was going to a tclOR backtracking point which was setting the loc to a completely disjoint part of the code having caused the error (see #12773). We replace the tclOR by a tclORELSE.
2020-08-11Merge PR #12815: [micromega] Fix bug#12790Vincent Laporte
Reviewed-by: vbgl
2020-08-11Merge PR #12814: [zify] fix for bug#12791Vincent Laporte
Reviewed-by: vbgl
2020-08-10[micromega] Fix bug#12790Frédéric Besson
zify used to generate many syntactic positivity constraints when translating a goal from nat to Z. For instance, to state that the product of 2 integers is positive. Instead, lia performs an interval analysis that is more semantic. The bug was that the interval analysis was performed after the elimination of equations. The current workaround is to perform interval analysis before and after eliminating equations. bla
2020-08-10[zify] fix for bug#12791Frédéric Besson
The elimination of let bindings is performing a convertibility check in order to deal with type aliases.
2020-08-10[ssr] turn "nothing to inject" into a real warning (fix #12746)Enrico Tassi
2020-08-06Actually use the default instance stored inside named_context_val.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 09:02:49 +0000