| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-11-25 | Make restrict_universe_context stronger. | Gaëtan Gilbert | |
| This fixes BZ#5717. Also add a test and fix a changed test. | |||
| 2017-11-25 | Fix obligations handling of universes anticipating stronger restrict | Matthieu Sozeau | |
| 2017-11-24 | [lib] Generalize Control.timeout type. | Emilio Jesus Gallego Arias | |
| We also remove some internal implementation details from the mli file, there due historical reasons. | |||
| 2017-11-24 | Use Evarutil.has_undefined_evars for tactic has_evar. | Gaëtan Gilbert | |
| 2017-11-24 | 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 | |
| This reduces conversions between ContextSet/UContext and encodes whether we are polymorphic by which constructor we use rather than using some boolean. | |||
| 2017-11-24 | When declaring constants/inductives use ContextSet if monomorphic. | Gaëtan Gilbert | |
| 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. | |||
| 2017-11-24 | 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 | |
| I think this only affects printing (in the new test you would get [Var (0)] when printing runwrap) but is still ugly. | |||
| 2017-11-24 | Register universe binders for record projections. | Gaëtan Gilbert | |
| 2017-11-24 | Stop exposing UState.universe_context and its Evd wrapper. | Gaëtan Gilbert | |
| 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). | |||
| 2017-11-24 | 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 | |
| Before sometimes there were lists and strings. | |||
| 2017-11-24 | Use type Universes.universe_binders. | Gaëtan Gilbert | |
| 2017-11-24 | A possible fix after PR#6158 (raw/glob generic printers for ltac values). | Hugo Herbelin | |
| Can the printers exploit the ability to now take an environment? | |||
| 2017-11-24 | Extending further PR#6047 (system to register printers for Ltac values). | Hugo Herbelin | |
| We generalize the possible use of levels to raw and glob printers. This is potentially useful for printing ltac expressions which are the glob level. | |||
| 2017-11-24 | Printing again "intros **" as "intros" by default. | Hugo Herbelin | |
| The rationale it that it is more common to do so and thus more "natural" (principle of writing less whenever possible). | |||
| 2017-11-24 | Fixes #5787 (printing of "constr:" lost in the move of constr to Generic). | Hugo Herbelin | |
| Was broken since 8.6. | |||
| 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 | |
| constructs. | |||
| 2017-11-24 | Fix deprecated syntax warning from vernacextend.mlp. | Gaëtan Gilbert | |
| 2017-11-24 | Merge PR #876: In omega or romega, recognizing Z and nat modulo conversion | Maxime Dénès | |
| 2017-11-24 | coq_makefile tests: build in easily removed temporary subdirectory. | Gaëtan Gilbert | |
| This allows us to avoid doing git clean. | |||
| 2017-11-24 | Fix coq-makefile ocamldoc call when configured with -annotate. | Gaëtan Gilbert | |
| Fixes #6120. | |||
| 2017-11-24 | Make byte on gitlab. | Gaëtan Gilbert | |
| Hopefully this will stop the intermittent test-suite/coq-makefile/findlib-package failures. | |||
| 2017-11-24 | Fixing failing mkdir in test-suite for coq-makefile. | Hugo Herbelin | |
| Calling the test a second time after a make clean was failing due to an existing "src" directory left by the first call. | |||
| 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-23 | Unify style of comments in file CUnix. | Hugo Herbelin | |
| 2017-11-23 | Quote file names which have spaces in "Print LoadPath". | Hugo Herbelin | |
| The primary concern is for clarity of reading. May it affects tools which would parse the output of "Print LoadPath"? Presumably, these tools would not support file names with spaces already, so this may have no impact. | |||
| 2017-11-23 | Add a function to surround filenames containing a space with quotes. | Hugo Herbelin | |
| 2017-11-23 | Surrounding a few places printing file names with quotes when a space occurs. | Hugo Herbelin | |
| 2017-11-23 | Make one more function robust in term_dnet.ml | Maxime Dénès | |
| Was actually forgotten in native-coq. | |||
| 2017-11-23 | Make some functions on terms more robust w.r.t new term constructs. | Maxime Dénès | |
| 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. | |||
| 2017-11-23 | Merge PR #6167: Fixing factorization of recursive notations with an atomic ↵ | Maxime Dénès | |
| separator | |||
| 2017-11-23 | 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 | Linter: do not lint untracked files. | Gaëtan Gilbert | |
| 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 | |
| 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. | |||
| 2017-11-23 | Fixing a 8.7 regression of ring_simplify in ArithRing. | Hugo Herbelin | |
| With help from Guillaume (see discussion at https://github.com/coq/coq/issues/6191). | |||
| 2017-11-23 | Truncate strings in votour to 1024 characters. | Pierre-Marie Pédrot | |
| Making it bigger is kind of useless, takes time and clutters the output for no real advantage. | |||
| 2017-11-23 | 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 | Bypass int and string representation in votour when it's incorrect. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |