aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
Commit message (Collapse)AuthorAge
* Correct some spelling errorsmasterGravatar Benjamin Barenblat2018-07-22
| | | | | | | | | | Lintian found some spelling errors in the Debian packaging for coq. Fix them most places they appear in the current source. (Don't change documentation anchor names, as that would invalidate external deeplinks.) This also fixes a bug in coqdoc: prior to this commit, coqdoc would highlight `instanciate` but not `instantiate`.
* Merge PR #7941: Extend QuestionMark to produce a better error message in ↵Gravatar Pierre-Marie Pédrot2018-07-19
|\ | | | | | | case of missing record field
| * change into QuestionMark defaultGravatar Siddharth Bhat2018-07-17
| |
| * Change QuestionMark for better record field missing error message.Gravatar Siddharth Bhat2018-07-17
| | | | | | | | | | | | | | | | | | | | While we were adding a new field into `QuestionMark`, we decided to go ahead and refactor the constructor to hold an actual record. This record now holds the name, obligations, and whether the evar represents a missing record field. This is used to provide better error messages on missing record fields.
* | Remove useless libobject in proof_usingGravatar Maxime Dénès2018-07-13
|/
* Merge PR #7898: Remove camlp4 remainsGravatar Emilio Jesus Gallego Arias2018-07-11
|\
| * Introduce a Pcoq.Entry module for functions that ought to be exported.Gravatar Pierre-Marie Pédrot2018-07-07
| | | | | | | | | | | | | | | | | | | | We deprecate the corresponding functions in Pcoq.Gram. The motivation is that the Gram module is used as an argument to Camlp5 functors, so that it is not stable by extension. Enforcing that its type is literally the one Camlp5 expects ensures robustness to extension statically. Some really internal functions have been bluntly removed. It is unlikely that they are used by external plugins.
| * Remove dead code that used to be there for CamlpX compatibility.Gravatar Pierre-Marie Pédrot2018-07-07
| | | | | | | | | | | | Part of this code has been introduced very recently in 7c62654 in spite of the existence of a proper API. This means that this should be better documented.
* | fix syntax of .mlgGravatar Vincent Laporte2018-07-03
| |
* | [vernac] use a record for the contents of the “deprecated” attributeGravatar Vincent Laporte2018-07-03
| |
* | [vernac] use plain strings as attribute namesGravatar Vincent Laporte2018-07-03
| | | | | | | | The concrete syntax is still restricted to identifiers.
* | [vernac] indentationGravatar Vincent Laporte2018-07-03
| |
* | [vernac] Generic syntax for flags/attributesGravatar Vincent Laporte2018-07-03
| |
* | [vernac] Generic parsing rules for attributesGravatar Vincent Laporte2018-07-03
| |
* | [vernac] Add a “deprecated” attributeGravatar Vincent Laporte2018-07-03
| |
* | Allow “Let”-defined coercionsGravatar Vincent Laporte2018-07-03
| |
* | [vernac] Concrete syntax for attributesGravatar Vincent Laporte2018-07-03
| |
* | [vernac] mk_atts: an atts record with default valuesGravatar Vincent Laporte2018-07-03
| |
* | [vernac] attribute_of_flagsGravatar Vincent Laporte2018-07-03
|/ | | | Elaborate a [atts] record out of a list of flags.
* Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commandsGravatar Pierre-Marie Pédrot2018-07-03
|\
* \ Merge PR #7703: Add an option to force parameters to be uniformGravatar Matthieu Sozeau2018-07-02
|\ \
| | * hints: add Hint Variables/Constants Opaque/Transparent commandsGravatar Matthieu Sozeau2018-07-02
| |/ |/| | | | | | | | | | | | | | | | | | | This gives user control on the transparent state of a hint db. Can override defaults more easily (report by J. H. Jourdan). For "core", declare that variables can be unfolded, but no constants (ensures compatibility with previous auto which allowed conv on closed terms) Document Hint Variables
* | Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension ↵Gravatar Emilio Jesus Gallego Arias2018-07-02
|\ \ | | | | | | | | | points of Camlp5
| | * Add flag Uniform Inductive ParametersGravatar Jasper Hugunin2018-07-01
| | |
| | * Implement uniform parameters in ComInductiveGravatar Jasper Hugunin2018-07-01
| | | | | | | | | | | | Don't allow notations attached to uniform inductives
* | | [api] Fix wrong deprecation warning (#7915)Gravatar Emilio Jesus Gallego Arias2018-07-01
| |/ |/| | | | | | | | | | | Fixes: #7915. Due to a change in the original misctypes removal PR, the deprecation notice went out of sync.
* | Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation ↵Gravatar Emilio Jesus Gallego Arias2018-07-01
|\ \ | | | | | | | | | format).
* \ \ Merge PR #7759: Workaround to fix #7731 (printing not splitting line at ↵Gravatar Emilio Jesus Gallego Arias2018-07-01
|\ \ \ | | | | | | | | | | | | break hint).
| | | * Port g_vernac to the homebrew GEXTEND parser.Gravatar Pierre-Marie Pédrot2018-06-29
| | | |
| | | * Port g_proofs to the homebrew GEXTEND parser.Gravatar Pierre-Marie Pédrot2018-06-29
| | | |
| | | * Use a homebrew parser to replace the GEXTEND extension points of Camlp5.Gravatar Pierre-Marie Pédrot2018-06-29
| |_|/ |/| | | | | | | | | | | | | | | | | | | | | | | The parser is stupid and the syntax is almost the same as the previous one. The only difference is that one needs to wrap OCaml code between { braces } so that quoting works out of the box. Files requiring such a syntax are handled specifically by the type system and need to have a .mlg extension instead of a .ml4 one.
| * | Workaround to fix #7731 (printing not splitting line at break hint).Gravatar Hugo Herbelin2018-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In some cases, Format's inner boxes inside an outer box act as break hints, even though there are already "better" break hints in the outer box. We work around this "feature" by not inserting a box around the default printing rule for a notation if there is no effective break points in the box. See https://caml.inria.fr/mantis/view.php?id=7804 for the related OCaml discussion.
| | * Fixes #7712 (an anomaly in reporting bad recursive notation format).Gravatar Hugo Herbelin2018-06-29
| |/
* | Merge PR #7080: Swapping Context and Constr and defining declarations on ↵Gravatar Maxime Dénès2018-06-29
|\ \ | | | | | | | | | constr in Constr
* | | Make Environ.globals abstract.Gravatar Gaëtan Gilbert2018-06-28
| |/ |/|
* | Merge PR #7866: Implementation of mutual records in the higher strataGravatar Maxime Dénès2018-06-28
|\ \
| | * Swapping Context and Constr: defining declarations on constr in Constr.Gravatar Hugo Herbelin2018-06-27
| |/ |/| | | | | | | | | | | | | | | This shall eventually allow to use contexts of declarations in the definition of the "Case" constructor. Basically, this means that Constr now includes Context and that the "t" types of Context which were specialized on constr are not defined in Constr (unfortunately using a heavy boilerplate).
* | Merge PR #7863: Remove Sorts.contentsGravatar Pierre-Marie Pédrot2018-06-27
|\ \
* \ \ Merge PR #7906: universes_of_constr don't include universes of monomorphic ↵Gravatar Pierre-Marie Pédrot2018-06-26
|\ \ \ | | | | | | | | | | | | constants
* \ \ \ Merge PR #7775: Fix handling of universe context for expanded program ↵Gravatar Maxime Dénès2018-06-26
|\ \ \ \ | | | | | | | | | | | | | | | obligations.
| | | * | Remove Sorts.contentsGravatar Gaëtan Gilbert2018-06-26
| |_|/ / |/| | |
| | * | universes_of_constr don't include universes of monomorphic constantsGravatar Gaëtan Gilbert2018-06-26
| | | | | | | | | | | | | | | | | | | | Apparently it was not useful. I don't remember what I was thinking when I added it.
* | | | Merge PR #7798: Remove hack skipping comparison of algebraic universes in ↵Gravatar Matthieu Sozeau2018-06-25
|\ \ \ \ | | | | | | | | | | | | | | | subtyping.
* \ \ \ \ Merge PR #7559: Existing Class noop when already a class + warning.Gravatar Matthieu Sozeau2018-06-25
|\ \ \ \ \
| | | | | * Handle mutual record at the vernac level.Gravatar Pierre-Marie Pédrot2018-06-24
| |_|_|_|/ |/| | | | | | | | | | | | | | Highly spaghetti code, hopefully works.
* | | | | Using more general information for primitive records.Gravatar Pierre-Marie Pédrot2018-06-23
| |_|_|/ |/| | | | | | | | | | | | | | | This brings more compatibility with handling of mutual primitive records in the kernel.
| | | * Fix handling of universe context for expanded program obligations.Gravatar Matthieu Sozeau2018-06-22
| |_|/ |/| | | | | | | | | | | | | | The universe context was dropped even though it isn't added to the global universes yet. Keep it so that it is properly defined with the constant the expanded obligation appears in.
| | * Remove hack skipping comparison of algebraic universes in subtyping.Gravatar Gaëtan Gilbert2018-06-22
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When inferring [u <= v+k] I replaced the exception and instead add [u <= v]. This is trivially sound and it doesn't seem possible to have the one without the other (except specially for [Set <= v+k] which was already handled). I don't know an example where this used to fail and now succeeds (the point was to remove an anomaly, but the example ~~~ Module Type SG. Definition DG := Type. End SG. Module MG : SG. Definition DG := Type : Type. Fail End MG. ~~~ now fails with universe inconsistency. Fix #7695 (soundness bug!).
* | Merge PR #7797: Remove reference name type.Gravatar Enrico Tassi2018-06-19
|\ \
* \ \ Merge PR #7801: [vernac] Add option to force building really mutual ↵Gravatar Enrico Tassi2018-06-19
|\ \ \ | | | | | | | | | | | | induction schemes
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-03 19:39:34 +0000