aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-02-19Merge PR #11636: Revert buggy commit mistakenly pushed with #11530Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-19Merge PR #11600: New syntax [Inductive Acc A R | x : Prop := ...]Emilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: maximedenes Reviewed-by: ppedrot
2020-02-19Revert "Granting #9516 and #9518 (support for numerals and strings in custom ↵Hugo Herbelin
entries)." This reverts commit 29919b725262dca76708192bde65ce82860747be. It was pushed by mistake as part of #11530. Sorry about it.
2020-02-19Overlays for Equations, QuickChick and Iris.Hugo Herbelin
2020-02-19Adding change log for #10832.Hugo Herbelin
2020-02-19Short allusion in refman on the existence of a generic and specific format.Hugo Herbelin
2020-02-19Addressing #6082 and #7766 (overriding format of notation).Hugo Herbelin
We do two changes: - We distinguish between a notion of format generically attached to notations and a new notion of format attached to interpreted notations. "Reserved Notation" attaches a format generically. "Notation" attaches the format specifically to the given interpretation, and additionally, attaches it generically if it is the first time the notation is defined. - We warn before overriding an explicitly reserved generic format, or a specific format.
2020-02-19Only parsing in Reserved Notation: turning notice into a warning.Hugo Herbelin
2020-02-19Choosing a standard format for the "rew dependent" notation.Hugo Herbelin
2020-02-19Preparing fix to #6082 and #7766: Renaming type scope_elem and its elements.Hugo Herbelin
This is in anticipation of defining a new type type specific_notation = LastLonelyNotation | NotationInScope
2020-02-19Remove the dependency in float.cmo and uint63.cmo for building votour.Hugo Herbelin
This was useless since PR #11247 and is a cause of failure in bytecode compilation on some exotic architectures (such as "armel").
2020-02-19Add doc/unreleased.rst to .gitignore.Théo Zimmermann
And remove outdated entries on tutorials.
2020-02-19[make] Fix makefile variable after plugin .v files moveEmilio Jesus Gallego Arias
This is a bug due to #11529
2020-02-19Fix #11549: Ltac2 is incompatible with $.Pierre-Marie Pédrot
We use the same kind of trick as the one we used for &IDENT, namely check that no space appear between the dollar sign and the identifier.
2020-02-19Fix #11552: Ltac2 breaks query commands during proofs.Pierre-Marie Pédrot
Actually, callers of the Pvernac.register_proof_mode function have to manually register the parsing of vernacular queries themselves. This probably qualifies as an oversight from myself.
2020-02-19ComInductive: use lbound=Prop iff non polymorphicGaëtan Gilbert
This avoids having to interp params and intern arities twice.
2020-02-18Merge PR #11530: Fixes custom entries precedence bugs (#11331 part)Pierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-02-18Merge PR #11529: [build] Consolidate stdlib's .v files under a single directory.Théo Zimmermann
Reviewed-by: Zimmi48
2020-02-18Deprecate unsafe_type_ofGaëtan Gilbert
2020-02-18Merge PR #10204: Remove `unsafe_type_of` from `Coercion`Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: mattam82
2020-02-18Updating reference manual and adding a change log entry.Hugo Herbelin
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2020-02-17Take "Implicit Types" into account when printing terms.Hugo Herbelin
2020-02-17Merge PR #11350: stdlib List: add [remove'] and [count_occ'] that use [filter]Hugo Herbelin
Reviewed-by: anton-trunov
2020-02-17Mini-improvements in when to skip coercions or explicitly print implicit args.Hugo Herbelin
If a return type is given to a match/if/let, then we are in context (and thus may skip coercions or not make explicit those implicit arguments inferable from context). Note that the notion of "inferable from context" remains anyway an approximation in the case of implicit arguments. The body of a fix/cofix is also in context. Also fixed an inconsistency with parsing in the scope used to print the body of a fix.
2020-02-17[coqdep] Tweak changelog after recent PRs.Emilio Jesus Gallego Arias
2020-02-17Merge PR #11593: Update bug report address in coqwc man page.Théo Zimmermann
Reviewed-by: Zimmi48
2020-02-17Merge PR #11614: Show apostrophes and backticks in HTML doc, too.Théo Zimmermann
Reviewed-by: Zimmi48
2020-02-17Merge PR #11589: [coqdep] Remove support for `-c` ocamldep replacement.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2020-02-17New syntax [Inductive Acc A R | x : Prop := ...]Gaëtan Gilbert
to control uniform parameters. This replaces the attribute.
2020-02-17Revert "Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)"Gaëtan Gilbert
This reverts commit bc2c1836ba4c878903288060bcb66a0ef1aaced6.
2020-02-16Show apostrophes and backticks in HTML, too.Jim Fehrle
2020-02-16Revert "Suite picking numeral notation"Hugo Herbelin
This reverts commit 03c48bb6943312e606b80b7af65b1ccb7122a386.
2020-02-16Suite picking numeral notationHugo Herbelin
Ceci est une suite à numeral notation in custom entries, cherchant à raffiner la compatibilité entre entrées. C'est mélangé avec le "pick" précédent, et c'est en chantier.
2020-02-16Granting #9516 and #9518 (support for numerals and strings in custom entries).Hugo Herbelin
2020-02-16Adding change log.Hugo Herbelin
2020-02-16Fixing bug #9521 (anomaly due to missing declaration of level in custom entry).Hugo Herbelin
This fixes also #9640 part 1.
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-16CoqIDE: allow opening multiple files at onceErika
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-14Apply suggestions from code reviewJason Gross
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2020-02-14test for x[i] notation not breaking Ltac parsingAndres Erbsen
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-11 04:17:37 +0000