aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Merge PR #486: Make some functions on terms more robust w.r.t new term ↵Gravatar Maxime Dénès2017-11-24
|\ | | | | | | constructs.
* \ Merge PR #876: In omega or romega, recognizing Z and nat modulo conversionGravatar Maxime Dénès2017-11-24
|\ \
* | | Update PR filter used by RM.Gravatar Maxime Dénès2017-11-24
| | |
* | | Merge PR #6197: [plugin] Remove LocalityFixme über hack.Gravatar Maxime Dénès2017-11-24
|\ \ \
| | | * Make one more function robust in term_dnet.mlGravatar Maxime Dénès2017-11-23
| | | | | | | | | | | | | | | | Was actually forgotten in native-coq.
| | | * Make some functions on terms more robust w.r.t new term constructs.Gravatar Maxime Dénès2017-11-23
| | | | | | | | | | | | | | | | | | | | | | | | Extending terms is notoriously difficult. We try to get more help from the compiler by making sure such an extension will trigger non exhaustive pattern matching warnings.
* | | | Merge PR #6167: Fixing factorization of recursive notations with an atomic ↵Gravatar Maxime Dénès2017-11-23
|\ \ \ \ | | | | | | | | | | | | | | | separator
* \ \ \ \ Merge PR #6203: Fix universe polymorphic Program obligations.Gravatar Maxime Dénès2017-11-23
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6186: [api] Miscellaneous consolidation.Gravatar Maxime Dénès2017-11-23
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6221: Add PR filter used by RM to the contributing guide.Gravatar Maxime Dénès2017-11-23
|\ \ \ \ \ \ \ | |_|_|_|_|_|/ |/| | | | | |
| * | | | | | Add PR filter used by RM to the contributing guide.Gravatar Maxime Dénès2017-11-23
| | | | | | |
| | | | | | * Adding ad hoc overlay for sf/vfa.Gravatar Hugo Herbelin2017-11-23
| | | | | | |
| | | | | | * Recognizing Z in romega up to conversion.Gravatar Hugo Herbelin2017-11-23
| | | | | | |
| | | | | | * Using is_conv rather than eq_constr to find `nat` or `Z` in omega.Gravatar Hugo Herbelin2017-11-23
| |_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Moving at the same to a passing "env sigma" style rather than passing "gl". Not that it is strictly necessary, but since we had to move functions taking only a "sigma" to functions taking also a "env", we eventually adopted the "env sigma" style. (The "gl" style would have been as good.) This answers wish #4717.
* | | | | | Merge PR #6200: Remove pidentref grammar entry.Gravatar Maxime Dénès2017-11-23
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #1092: [stm] [doc] Add some documentation to obscure AsyncTaskQueueGravatar Maxime Dénès2017-11-23
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6123: Nix fileGravatar Maxime Dénès2017-11-23
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6189: Disable whitespace linter for .out files.Gravatar Maxime Dénès2017-11-23
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6187: Check findlib version in configure (fix #4270).Gravatar Maxime Dénès2017-11-23
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6192: Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Gravatar Maxime Dénès2017-11-23
|\ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / / / / |/| | | | | | | | | |
| | | | | | | | | | * [plugin] Remove LocalityFixme über hack.Gravatar Emilio Jesus Gallego Arias2017-11-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | To that extent we introduce a new prototype vernacular extension macro `VERNAC COMMAND FUNCTIONAL EXTEND` that will take a function with the proper parameters and attributes. This of course needs more refinement, in particular we should move `vernac_command` to its own file and make `Vernacentries` consistent wrt it.
| | | | | | | | | | * [plugin] Encapsulate modifiers to vernac commands.Gravatar Emilio Jesus Gallego Arias2017-11-22
| |_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a continuation on #6183 and another step towards a more functional interpretation of commands. In particular, this should allow us to remove the locality hack.
| | | | | | | * | | [api] A few more minor deprecation notices.Gravatar Emilio Jesus Gallego Arias2017-11-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Note the problem with `create_evar_defs`.
| | | | | | | * | | [api] Re-enable deprecation warnings.Gravatar Emilio Jesus Gallego Arias2017-11-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | With a bit of care we can enable full deprecation warnings again in this funny file.
| | | | | | | * | | [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We mirror the structure of EConstr and move the destructors from `Term` to `Constr`. This is a step towards having a single module for `Constr`.
| | | | | | | | * | Fix universe polymorphic Program obligations.Gravatar Matthieu Sozeau2017-11-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The universes of the obligations should all be non-algebraic as they might appear in instances of other obligations and instances only take non-algebraic universes as arguments.
| | | | | | | * | | [api] Miscellaneous consolidation + moves to engine.Gravatar Emilio Jesus Gallego Arias2017-11-21
| |_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We deprecate a few functions that were deprecated in the comments plus we place `Nameops` and `Univops` in engine where they do seem to belong in the large picture of code organization.
* | | | | | | | | Merge PR #6173: [printing] Deprecate all printing functions accessing the ↵Gravatar Maxime Dénès2017-11-21
|\ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | global proof.
| | | | | | * | | | [stm] [doc] Add some documentation to AsyncTaskQueue APIGravatar Emilio Jesus Gallego Arias2017-11-21
| |_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As a bonus we remove some trailing whitespace, and implement a couple of hints suggested in the discussion.
| * | | | | | | | [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
|/ / / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We'd like to handle proofs functionally we thus recommend not to use printing functions without an explicit context. We also adapt most of the code, making more explicit where the printing environment is coming from. An open task is to refactor some code so we gradually make the `Pfedit.get_current_context ()` disappear.
* | | | | | | | Merge PR #6185: [parser] Remove unnecessary statically initialized hook.Gravatar Maxime Dénès2017-11-21
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6181: [proof] Attempt to deprecate some V82 parts of the proof API.Gravatar Maxime Dénès2017-11-21
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6178: Have the coq_makefile timing test-suite print moreGravatar Maxime Dénès2017-11-21
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6168: Add Equations to CIGravatar Maxime Dénès2017-11-21
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6113: Extra work on ltac printing: fixing #5787, some parenthesesGravatar Maxime Dénès2017-11-21
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | |
| * | | | | | | | | | | Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).Gravatar Hugo Herbelin2017-11-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Was broken since 8.6.
| | | | | | | | | | | * Fixing factorization of recursive notations in the case of an atomic separator.Gravatar Hugo Herbelin2017-11-20
| |_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This addresses a limitation found in math-comp seq.v file. See the example in test suite file success/Notations2.v. To go further and accept recursive notations with a separator made of several tokens, and assuming camlp5 unchanged, one would need to declare an auxiliary entry for this sequence of tokens and use it as an "atomic" (non-terminal) separator. See PR #6167 for details.
| | | | | | | | | | * Remove pidentref grammar entry.Gravatar Gaëtan Gilbert2017-11-20
| |_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | Replaced by ident_decl in #688.
| | | | | | | | * | Disable whitespace linter for .out files.Gravatar Gaëtan Gilbert2017-11-20
| | | | | | | | | |
| | | | | | | * | | Check findlib version in configure (fix #4270).Gravatar Gaëtan Gilbert2017-11-20
| | | | | | | | | |
* | | | | | | | | | Merge PR #6188: Rename coq-inferior.el -> inferior-coq.el to match provided ↵Gravatar Maxime Dénès2017-11-20
|\ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | feature.
* \ \ \ \ \ \ \ \ \ \ Merge PR #6184: [lib] Minor pending cleanup to consolidate helper function.Gravatar Maxime Dénès2017-11-20
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6183: [plugins] Prepare plugin API for functional handling of state.Gravatar Maxime Dénès2017-11-20
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6166: Fix regression in treating Defined as definedGravatar Maxime Dénès2017-11-20
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6163: [dev] Remove deprecation warning from `base_include`Gravatar Maxime Dénès2017-11-20
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6161: Fix micromega.ml to match generated file and enforce match ↵Gravatar Maxime Dénès2017-11-20
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | in make.
| | | | | | | | * | | | | | | | Add Equations to CIGravatar Matthieu Sozeau2017-11-20
| | | | | | | | | |_|_|_|_|/ / | | | | | | | | |/| | | | | |
* | | | | | | | | | | | | | | Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 ↵Gravatar Maxime Dénès2017-11-20
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (clause "where" with implicit arguments)
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces ↵Gravatar Maxime Dénès2017-11-20
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | unbound rel
| | | | | | | | | | | | | * | | Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Gravatar Gaëtan Gilbert2017-11-19
| |_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 20:20:37 +0000