aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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.
2020-02-11Reinforcing the role of type "typing_constraint".Hugo Herbelin
WithoutTypeConstraint says it can be a term. In particular, if it has manual implicit arguments, these will be allowed only in leading lambdas. I.e. it can start with "fun {x}" but not with "forall {x}". New constructor UnknownIfTermOrType allows to be both a term or a type. In particular, if it allowed start both with "fun {x}" and "forall {x}".
2020-02-11Lately adding a changelog for PR#10202.Hugo Herbelin
2020-02-11Remove unused Environ.push_constraints_to_envGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 16:13:36 +0000