| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Restrict universe context when declaring constants in obligations. |  Gaëtan Gilbert | 2017-11-25 |
| | | |||
| * | Fix #5347: unify declaration of axioms with and without bound univs. | Gaëtan Gilbert | 2017-11-25 |
| | | | | | | | | | | Note that this makes the following syntax valid: Axiom foo@{i} bar : Type@{i}. (ie putting a universe declaration on the first axiom in the list, the declaration then holds for the whole list). | ||
| * | Fix interpretation of global universes in univdecl constraints. | Gaëtan Gilbert | 2017-11-25 |
| | | | | | Also nicer error when the constraints are impossible. | ||
| * | Forbid repeated names in universe binders. | Gaëtan Gilbert | 2017-11-25 |
| | | |||
| * | Universe binders survive sections, modules and compilation. | Gaëtan Gilbert | 2017-11-25 |
| | | |||
| * | Allow local universe renaming in Print. | Gaëtan Gilbert | 2017-11-25 |
| | | |||
| * | Make restrict_universe_context stronger. | Gaëtan Gilbert | 2017-11-25 |
| | | | | | | | This fixes BZ#5717. Also add a test and fix a changed test. | ||
| * | Fix obligations handling of universes anticipating stronger restrict |  Matthieu Sozeau | 2017-11-25 |
| | | |||
| * | In close_proof only check univ decls with the restricted context. | Gaëtan Gilbert | 2017-11-24 |
| | | |||
| * | Use Entries.constant_universes_entry more. | Gaëtan Gilbert | 2017-11-24 |
| | | | | | | | This reduces conversions between ContextSet/UContext and encodes whether we are polymorphic by which constructor we use rather than using some boolean. | ||
| * | When declaring constants/inductives use ContextSet if monomorphic. | Gaëtan Gilbert | 2017-11-24 |
| | | | | | | | | | Also use constant_universes_entry instead of a bool flag to indicate polymorphism in ParameterEntry. There are a few places where we convert back to ContextSet because check_univ_decl returns a UContext, this could be improved. | ||
| * | restrict_universe_context: do not prune named universes. | Gaëtan Gilbert | 2017-11-24 |
| | | |||
| * | Fix defining non primitive projections with abstracted universes. | Gaëtan Gilbert | 2017-11-24 |
| | | | | | | I think this only affects printing (in the new test you would get [Var (0)] when printing runwrap) but is still ugly. | ||
| * | Register universe binders for record projections. | Gaëtan Gilbert | 2017-11-24 |
| | | |||
| * | Stop exposing UState.universe_context and its Evd wrapper. | Gaëtan Gilbert | 2017-11-24 |
| | | | | | | | We can enforce properties through check_univ_decl, or get an arbitrary ordered context with UState.context / Evd.to_universe_context (the later being a new wrapper of the former). | ||
| * | Separate checking univ_decls and obtaining universe binder names. | Gaëtan Gilbert | 2017-11-24 |
| | | |||
| * | Use Maps and ids for universe binders | Gaëtan Gilbert | 2017-11-24 |
| | | | | | Before sometimes there were lists and strings. | ||
| * | Use type Universes.universe_binders. | Gaëtan Gilbert | 2017-11-24 |
| | | |||
| * | Merge PR #6231: Fix link to Recursive Make Considered Harmful |  Maxime Dénès | 2017-11-24 |
| |\ | |||
| * \ | Merge PR #6205: Fixing a 8.7 regression of ring_simplify in ArithRing | Maxime Dénès | 2017-11-24 |
| |\ \ | |||
| * \ \ | Merge PR #486: Make some functions on terms more robust w.r.t new term ↵ | Maxime Dénès | 2017-11-24 |
| |\ \ \ | | | | | | | | | | | | | constructs. | ||
| * \ \ \ | Merge PR #876: In omega or romega, recognizing Z and nat modulo conversion | Maxime Dénès | 2017-11-24 |
| |\ \ \ \ | |||
| * | | | | | Update PR filter used by RM. | Maxime Dénès | 2017-11-24 |
| | | | | | | |||
| * | | | | | Merge PR #6197: [plugin] Remove LocalityFixme über hack. | Maxime Dénès | 2017-11-24 |
| |\ \ \ \ \ | |||
| | | | * | | | Make one more function robust in term_dnet.ml | Maxime Dénès | 2017-11-23 |
| | | | | | | | | | | | | | | | | | | | | | | | | | Was actually forgotten in native-coq. | ||
| | | | * | | | Make some functions on terms more robust w.r.t new term constructs. | Maxime Dénès | 2017-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 ↵ | Maxime Dénès | 2017-11-23 |
| |\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | separator | ||
| * \ \ \ \ \ \ | Merge PR #6203: Fix universe polymorphic Program obligations. | Maxime Dénès | 2017-11-23 |
| |\ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ | Merge PR #6186: [api] Miscellaneous consolidation. | Maxime Dénès | 2017-11-23 |
| |\ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ | Merge PR #6221: Add PR filter used by RM to the contributing guide. | Maxime Dénès | 2017-11-23 |
| |\ \ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / / |/| | | | | | | | | |||
| | | | | | | | | * | Fix link to Recursive Make Considered Harmful | Gaëtan Gilbert | 2017-11-23 |
| | |_|_|_|_|_|_|/ |/| | | | | | | | |||
| | * | | | | | | | Add PR filter used by RM to the contributing guide. | Maxime Dénès | 2017-11-23 |
| | | | | | | | | | |||
| | | | | | | * | | Adding ad hoc overlay for sf/vfa. |  Hugo Herbelin | 2017-11-23 |
| | | | | | | | | | |||
| | | | | | | * | | Recognizing Z in romega up to conversion. | Hugo Herbelin | 2017-11-23 |
| | | | | | | | | | |||
| | | | | | | * | | Using is_conv rather than eq_constr to find `nat` or `Z` in omega. | Hugo Herbelin | 2017-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. | ||
| | | | | | | * | Fixing a 8.7 regression of ring_simplify in ArithRing. | Hugo Herbelin | 2017-11-23 |
| | |_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | With help from Guillaume (see discussion at https://github.com/coq/coq/issues/6191). | ||
| * | | | | | | Merge PR #6200: Remove pidentref grammar entry. | Maxime Dénès | 2017-11-23 |
| |\ \ \ \ \ \ | |||
| * \ \ \ \ \ \ | Merge PR #1092: [stm] [doc] Add some documentation to obscure AsyncTaskQueue | Maxime Dénès | 2017-11-23 |
| |\ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ | Merge PR #6123: Nix file | Maxime Dénès | 2017-11-23 |
| |\ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ | Merge PR #6189: Disable whitespace linter for .out files. | Maxime Dénès | 2017-11-23 |
| |\ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ | Merge PR #6187: Check findlib version in configure (fix #4270). | Maxime Dénès | 2017-11-23 |
| |\ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ | Merge PR #6192: Fix #5790: make Hint Resolve <- respect univ polymorphism flag. | Maxime Dénès | 2017-11-23 |
| |\ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / / / / |/| | | | | | | | | | | |||
| | | | | | | | | | | * | [plugin] Remove LocalityFixme über hack. |  Emilio Jesus Gallego Arias | 2017-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. | Emilio Jesus Gallego Arias | 2017-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. | Emilio Jesus Gallego Arias | 2017-11-22 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Note the problem with `create_evar_defs`. | ||
| | | | | | | | * | | | [api] Re-enable deprecation warnings. | Emilio Jesus Gallego Arias | 2017-11-22 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | With a bit of care we can enable full deprecation warnings again in this funny file. | ||
| | | | | | | | * | | | [api] Deprecate Term destructors, move to Constr | Emilio Jesus Gallego Arias | 2017-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. | Matthieu Sozeau | 2017-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. | Emilio Jesus Gallego Arias | 2017-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 ↵ | Maxime Dénès | 2017-11-21 |
| |\ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | global proof. | ||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |