aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-07-29Miscellaneous uniformization of typography in chapter syntax extensions.Hugo Herbelin
2018-07-29Documenting custom entries in the reference manual + CHANGES.Hugo Herbelin
2018-07-29Store marshallable data in the custom entry summary.Pierre-Marie Pédrot
2018-07-29Supporting locality flag for custom entries + compatibility with modules.Hugo Herbelin
Also prevents to use an entry name already defined.
2018-07-29Do not treat curly brackets specially in custom entries.Hugo Herbelin
2018-07-29Classify "Declare Custom" as VtNow for the stm.Hugo Herbelin
When parsing of a document shall be possible independently of interpretation, this shall however be indicated as shall be interpreted now so that the notation commands coming next work.
2018-07-29Renaming ETName and ETReference so as to fit the user-visible terminology.Hugo Herbelin
ETName -> ETIdent ETReference -> ETGlobal
2018-07-29Adding support for custom entries in notations.Hugo Herbelin
- New command "Declare Custom Entry bar". - Entries can have levels. - Printing is done using a notion of coercion between grammar entries. This typically corresponds to rules of the form 'Notation "[ x ]" := x (x custom myconstr).' but also 'Notation "{ x }" := x (in custom myconstr, x constr).'. - Rules declaring idents such as 'Notation "x" := x (in custom myconstr, x ident).' are natively recognized. - Rules declaring globals such as 'Notation "x" := x (in custom myconstr, x global).' are natively recognized. Incidentally merging ETConstr and ETConstrAsBinder. Noticed in passing that parsing binder as custom was not done as in constr. Probably some fine-tuning still to do (priority of notations, interactions between scopes and entries, ...). To be tested live further.
2018-07-29A test on the different ways to indicate the levels of a rule.Hugo Herbelin
This is in preparation of changes in level_eq, to check that the semantics is preserved.
2018-07-29Synchronizing "grammars by name" with backtrack (custom entries shall be ↵Hugo Herbelin
added incrementally).
2018-07-28Merge PR #8077: Fix #7291: unify tactic should have more descriptive error ↵Hugo Herbelin
messages.
2018-07-28Merge PR #8160: Improved chapters 'Implicit Coercions' and 'Canonical ↵Théo Zimmermann
Structures' of the Reference Manual.
2018-07-28Merge PR #8148: Doc: preliminary work before #7291 which add an "Unable to ↵Théo Zimmermann
unify" message
2018-07-27Merge PR #8174: [ci] Remove CircleCI setup.Gaëtan Gilbert
2018-07-27Merge PR #8173: Missing backslash in a documentation file.Théo Zimmermann
2018-07-27[ci] Remove CircleCI setup.Emilio Jesus Gallego Arias
GitLab setup is quite stable these days thanks to the work of many people and `coqbot`. We decided to keep CircleCI support for a while as a safeguard in case something happened in the migration to GitLab, but these days we are just wasting resources to them and to us. As I'm afraid CircleCI won't scale for us, the time to remove it has arrived. Still, CircleCI had some awesome functionality that GitLab's CI doesn't offer yet, see the links at: https://github.com/coq/coq/issues/6919#issuecomment-395885573 - https://gitlab.com/gitlab-org/gitlab-ce/issues/29347 - https://gitlab.com/gitlab-org/gitlab-ce/issues/35222 - https://gitlab.com/gitlab-org/gitlab-ce/issues/41947 - https://gitlab.com/gitlab-org/gitlab-ce/issues/47063
2018-07-27Missing backslash in the documentation file.Martin Bodin
2018-07-27Merge PR #8164: Add information to option type errorsEnrico Tassi
2018-07-27Merge PR #8166: Fix Search query in CoqIDE.Enrico Tassi
2018-07-27Merge PR #8103: Coercions cleanup: use GlobRef.t instead of constrEnrico Tassi
2018-07-27Merge PR #8141: Diff option in CoqIDEEnrico Tassi
2018-07-26Merge PR #8101: Remove ClosedModule and ClosedSection from libstackEnrico Tassi
2018-07-26Fix Search query in CoqIDE.Pierre-Marie Pédrot
For some reason the code was just doing random stuff that did not make sense.
2018-07-26Improved chapters 'Implicit Coercions' and 'Canonical Structures' of the ↵Zeimer
Reference Manual.
2018-07-26Add information to option type errorsTej Chajed
Print the expected and actual types for the option value (which is one of bool, int, or string).
2018-07-26Replace iter + ref by fold_leftMaxime Dénès
2018-07-26restore reduction of coercion to eventually expose a constructorEnrico Tassi
2018-07-26Coercions cleanup: use GlobRef.t instead of constrMaxime Dénès
2018-07-26Merge PR #8100: Use just one object declaration for all global universe ↵Pierre-Marie Pédrot
additions
2018-07-26Merge PR #8050: Cleanup VERNAC EXTENDMaxime Dénès
2018-07-26Expose the diff printing option as an UI entry in CoqIDE.Pierre-Marie Pédrot
2018-07-26Do not set diff printing on by default in CoqIDE.Pierre-Marie Pédrot
2018-07-26Merge PR #8122: Fix #8119: anomalies in vm_compute with let and evars.Maxime Dénès
2018-07-26Merge PR #7786: In "redundant clause" pattern-matching error, show also the ↵Pierre-Marie Pédrot
pattern (closes #7777)
2018-07-26Merge PR #8084: Properly disable native compilation when -native-compiler is ↵Maxime Dénès
unset.
2018-07-26Merge PR #7274: Avoiding introducing dependency on the indices of a term ↵Pierre-Marie Pédrot
which has no matching clauses.
2018-07-26Merge PR #8150: Fix static declaration of plugins in coqpp.Emilio Jesus Gallego Arias
2018-07-25Remove object duplication for Constraint command.Gaëtan Gilbert
2018-07-25Hints use Declare to declare universes instead of a custom object.Gaëtan Gilbert
2018-07-25Merge PR #7859: Remove himsg.pr_puniverses, use @{} for universe printing in ↵Pierre-Marie Pédrot
errors
2018-07-25Merge PR #8133: Fixes #8126: issue with notations and nested applicationsEmilio Jesus Gallego Arias
2018-07-25Merge PR #734: [travis] Also run coqchk on HoTTEmilio Jesus Gallego Arias
2018-07-25In "redundant clause" pattern-matching error, show also the pattern (#7777).Hugo Herbelin
This is particularly useful when the pattern is part of a disjunction. Maybe this could be improved though, not mentioning the pattern when there is no disjunction, but that would be more work.
2018-07-25Optimized dependencies for pattern-matching on only trivial patterns.Hugo Herbelin
If a term is matched only against variables, it will not introduce a "match" and thus, even if the term is of an inductive type, its indices will not be taken into account in the current algorithm (though one could imagine an algorithm which does an expansion specially in order to filter on indices). This allows to tell the unification not to use dependencies which the pattern-matching algorithm is not able to exploit in practice. See example in file 2733.v.
2018-07-25Fix static declaration of plugins in coqpp.Pierre-Marie Pédrot
The module was not properly registered with dynlink turned off, leading to a failure of compilation of the prelude.
2018-07-25Doc: preliminary work before #7291 which add an "Unable to unify" message.Hugo Herbelin
We adopt the convention that error messages with a template use the sphinx syntax used in defining syntax rules.
2018-07-25Add overlay for EquationsGaëtan Gilbert
2018-07-25Remove himsg.pr_puniverses, use @{} for universe printing in errorsMaxime Dénès
Replaces #6401.
2018-07-25Merge PR #7889: Cleanup reduction effects: they only work on constants.Pierre-Marie Pédrot
2018-07-25Merge PR #8139: Replace all the CoInductives with Variants in the SSR pluginEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 14:27:01 +0000