aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-02-15Dead code in Egramcoq.adjust_level.Hugo Herbelin
2020-02-15Fixing a precedence printing bug with custom entries.Hugo Herbelin
Insertion of coercion to manage precedence of custom entries are treated in constrextern.ml, while ppconstr.ml is only about the management of precedences for constr.
2020-02-15Fixes #11331 (unexpected level collisions between custom entries and constr).Hugo Herbelin
There was a collision at the time of interpreting subentries (in metasyntax.ml) but also at the time of "optimizing" the entries (in egramcoq.ml). Also fixes #9517, fixes #9519, fixes #9640 (part 3).
2020-02-14Merge pull request #11605 from ppedrot/ltac2-annotate-match-branchKenji Maillard
Annotate Ltac2 match macro variables with their type.
2020-02-14Merge PR #11557: Use thunks to univ instead of lazy constr for template typingPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-02-14Annotate Ltac2 match macro variables with their type.Pierre-Marie Pédrot
This prevents some warnings to be dropped when the variables are not used at the right type. See #11603 for a motivation.
2020-02-14Merge PR #11599: Spell out index entry suffixes in main index, e.g. ↵Théo Zimmermann
"(tactic)" instead of "(tacn)" Reviewed-by: Zimmi48
2020-02-14Merge PR #11468: [doc] fix typo & update release-process.md for opam/docker ↵Théo Zimmermann
packaging Reviewed-by: Zimmi48 Ack-by: jfehrle
2020-02-14Overlay for Inductive.type_of_inductive doesn't take an envGaëtan Gilbert
2020-02-14Use thunks to univ instead of lazy constr for template typingGaëtan Gilbert
2020-02-14Merge PR #11584: Add #[uniform] and #[nonuniform] (for Uniform Inductive ↵Maxime Dénès
Parameters) Reviewed-by: Matafou Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2020-02-13Spell out the entry suffix in the main indexJim Fehrle
Ex: "(tactic)" instead of "(tacn)"
2020-02-13Merge PR #11427: Dispatch code ownership of files in dev/doc.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: gares
2020-02-13Merge PR #11450: Publishing a new version on Zenodo: not a relevant step for ↵Emilio Jesus Gallego Arias
beta versions. Reviewed-by: ejgallego
2020-02-13Merge PR #11441: Add explicit types to changelog entries that were still ↵Emilio Jesus Gallego Arias
missing them. Reviewed-by: ejgallego
2020-02-13Merge PR #11564: Recognize Default Proof Using in STMEnrico Tassi
Ack-by: gares
2020-02-13Merge PR #11417: Move kind_of_type from the kernel to EConstr.Enrico Tassi
Reviewed-by: SkySkimmer Reviewed-by: gares
2020-02-13Merge PR #11098: Let Arguments support anonymous implicit argumentsEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2020-02-13Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)Gaëtan Gilbert
2020-02-13Delete unused commentGaëtan Gilbert
2020-02-13Don't duplicate the inductive keyword for each block elt when parsingGaëtan Gilbert
2020-02-13Merge PR #11407: [mltop] Store digest of modules used to compile files.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: maximedenes
2020-02-13Merge PR #11521: Remove Goptions.opt_name fieldPierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-02-13Merge PR #11457: [toplevel] Refactor control loopHugo Herbelin
Ack-by: SkySkimmer Ack-by: gares Reviewed-by: herbelin
2020-02-13Merge PR #11424: Check instance length in type_of_{inductive,constructor}Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-02-13Merge PR #11577: [nix] Fix building of the documentationThéo Zimmermann
Reviewed-by: Zimmi48
2020-02-13Arguments: removing the restriction to set an anonymous parameter implicit.Hugo Herbelin
This was already possible manually using "{ _ }" in the type of declaration. This was also possible for type classes. So, no reason to forbid in Arguments.
2020-02-13Implicit arguments: Fixing count of the position in compute_implicit_statuses.Hugo Herbelin
2020-02-12Merge PR #11582: Split unicoq out of ci-mtac2.sh (keeping 1 CI job)Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-12Split unicoq out of ci-mtac2.sh (keeping 1 CI job)Gaëtan Gilbert
No reason to have them in the same .sh
2020-02-12[toplevel] Make toplevel loop tail-recursive againEmilio Jesus Gallego Arias
In previous refactorings `vernac_loop` stopped being tail-recursive, we refactor code a bit and make it back into tail-recursive form.
2020-02-12[toplevel] Refactor control loopEmilio Jesus Gallego Arias
We refactor control loop a bit to make the code more readable: - the code for unhandled exception is not needed anymore as it cannot happen. - we move the processing of toplevel commands to its own function - we split away diff-specific functions.
2020-02-12Merge PR #11544: Cleanup some globref related manipulationsPierre-Marie Pédrot
Reviewed-by: herbelin Reviewed-by: ppedrot
2020-02-12overlay for removal of optnameGaëtan Gilbert
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
The standard use is to repeat the option keywords in lowercase, which is basically useless. En passant add doc entry for Dump Arith.
2020-02-12Merge PR #11569: Remove unused Environ.push_constraints_to_envPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-02-12Merge PR #11563: Mini improvement of the formatting rule for printing fix ↵Gaëtan Gilbert
and cofix Reviewed-by: SkySkimmer
2020-02-12Check instance length in type_of_{inductive,constructor}Gaëtan Gilbert
2020-02-12Standardize constr -> globref operations to use destRef/isRef/isRefXGaëtan Gilbert
Instead of various termops and globnames aliases.
2020-02-12ReferenceVariables error contains a globref instead of a constrGaëtan Gilbert
The previous system was from before globref was in the kernel.
2020-02-12Merge PR #11556: [coqdep] mli cleanup, remove unused functionsGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-02-12Merge PR #11546: Remove the Template Check option.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: Zimmi48
2020-02-12[nix] Fix building of the documentationVincent Laporte
The interpreter directive of “doc/stdlib/make-library-index” must be patched.
2020-02-12Merge PR #11573: Fixing extra space in front of keywords in Print GrammarEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-11Merge PR #11509: Add changelog and fixes for #10202Emilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2020-02-11Fixing extra space in "Print Grammar" (i.e. Grammar.Entry.print in Gramlib).Hugo Herbelin
2020-02-11Merge PR #11494: Remove fiat-crypto-legacy from CIGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: gares Reviewed-by: ppedrot Reviewed-by: vbgl
2020-02-11Remove fiat-crypto-legacy from CIMaxime Dénès
Motivations: - We should have only maintained developments in our CI - `make ci-fiat-crypto-legacy` takes about 15 mins before the first call to `coqc`, making it unusable to work on overlays - The coding style of this development is so fragile that adapting to any change of behavior requires diffing gigabytes of Ltac traces. @mattam82 and I have been blocked for 6 months this way, when working on unifall. I understand this development was meant to stress-test some components like printing, but I think the trade-off is bad. We should rather come up with specialized test suites for these components.
2020-02-11Document the ability to use manual implicit arguments in subexpressions.Hugo Herbelin
2020-02-11Fixing some residual bugs of PR #10202 (manual implicit args in subterms).Hugo Herbelin
- Implicit arguments in the return clause and in the branches of a match were not checked. - Implicit arguments in each declaration of intern_context were not restarted. - Additionally, in intern_context, we take into account ids from the env on top of which intern_context is called. - A better approximation of the check for manual implicit in notations improved (though not fully correct because the exact context of interpretation of a binder in a notation with recursive binders is not known). We also rename impl_binder_index into binder_block_names in anticipation of checking redundancies also for non-implicit arguments.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 08:26:35 +0000