| Commit message (Expand) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| | | | | | | | | | | | | | * | Fix obligations handling of universes anticipating stronger restrict |  Matthieu Sozeau | 2017-11-25 | |
| | | | | | | * | | | | | | | | [lib] Generalize Control.timeout type. |  Emilio Jesus Gallego Arias | 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 | 2017-11-24 | |
| | | | | | | | | | | | * | When declaring constants/inductives use ContextSet if monomorphic. | Gaëtan Gilbert | 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 | 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 | 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 | 2017-11-24 | |
| | | | | | | | | | | | * | 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 constr... | Maxime Dénès | 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 | 2017-11-24 | |
| | |_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | ||||
| | | | | | | | | | | | * | | Fix coq-makefile ocamldoc call when configured with -annotate. | Gaëtan Gilbert | 2017-11-24 | |
| | |_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | ||||
| | | | | | | | | | * | | | Make byte on gitlab. | Gaëtan Gilbert | 2017-11-24 | |
| | | | | | | | | | | | * | Fixing failing mkdir in test-suite for coq-makefile. |  Hugo Herbelin | 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 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | ||||
| | | | | | | | * | | | | | Unify style of comments in file CUnix. | Hugo Herbelin | 2017-11-23 | |
| | | | | | | | * | | | | | Quote file names which have spaces in "Print LoadPath". | Hugo Herbelin | 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 | 2017-11-23 | |
| | | | * | | | | | | | | Make some functions on terms more robust w.r.t new term constructs. | Maxime Dénès | 2017-11-23 | |
| | | | | |_|_|_|_|/ / | | | |/| | | | | | | ||||
| * | | | | | | | | | | Merge PR #6167: Fixing factorization of recursive notations with an atomic se... | Maxime Dénès | 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 | 2017-11-23 | |
| | |_|_|_|_|/ / / / / |/| | | | | | | | | | ||||
| | | | | | | * | | | | Fixing a 8.7 regression of ring_simplify in ArithRing. | Hugo Herbelin | 2017-11-23 | |
| | |_|_|_|_|/ / / / |/| | | | | | | | | ||||
| | | | | | | | * | | Truncate strings in votour to 1024 characters. |  Pierre-Marie Pédrot | 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 | 2017-11-23 | |
| | | | | | | | | | * | | Tail-recursive list traversal in votour. | Pierre-Marie Pédrot | 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 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | ||||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |