aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-02-16Mini-factorization in vernac grammar.Hugo Herbelin
Unfortunately, we cannot factorize further | x = IDENT; "at"; lev = level; b = OPT constr_as_binder_kind | x = IDENT; b = constr_as_binder_kind without losing the rule | x = IDENT; typ = syntax_extension_type
2020-02-16Custom entries: accept that no level is mentioned for a subentry.Hugo Herbelin
If it is for an internal non-terminal then: - if for a subentry different from constr, it refers to the head of the subentry - if in constr, it is 200 by convention If it is on the border of a rule, then: - if it is in a subentry different from the entry it lives, it refers to the head of the subentry (or 200 by convention if in constr) - if it is in the same entry, the rule for associativity tells if a SELF, a NEXT, or (if on the right) a LEVEL
2020-02-15Reusing type production_level for the result of adjust_level.Hugo Herbelin
2020-02-15Reorganize type "production_level" along a more intuitive structure.Hugo Herbelin
NextLevel = at next level NumLevel n = at level n DefaultLevel = <no mention of level>
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 05:42:17 +0000