Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Restore a fast path in EConstr instance normalization. | Pierre-Marie Pédrot | 2017-04-01 |
* | Using delayed universe instances in EConstr. | Pierre-Marie Pédrot | 2017-04-01 |
* | Actually exporting delayed universes in the EConstr implementation. | Pierre-Marie Pédrot | 2017-04-01 |
* | Make the Constr.kind_of_term type parametric in sorts and universes. | Pierre-Marie Pédrot | 2017-03-31 |
* | Ensuring proper cast invariants in EConstr.kind. | Pierre-Marie Pédrot | 2017-03-31 |
* | Revert "Specially crafted EConstr.kind to be more efficient." | Pierre-Marie Pédrot | 2017-03-31 |
* | Specially crafted EConstr.kind to be more efficient. | Pierre-Marie Pédrot | 2017-03-30 |
* | Merge branch 'trunk' into pr379 | Maxime Dénès | 2017-03-29 |
|\ | |||
* | | Fix call to broken unsafe_type_of in apply tactic. | Maxime Dénès | 2017-03-29 |
* | | Revert to incorrect heuristic in apply. | Maxime Dénès | 2017-03-28 |
| * | Fixing missing PropFacts.v in Logic/vo.itarget. | Hugo Herbelin | 2017-03-28 |
* | | Mathcomp overlay. | Maxime Dénès | 2017-03-25 |
* | | Fix interpretation of Ltac patterns episode 2. | Maxime Dénès | 2017-03-24 |
* | | Merge branch 'trunk' into pr379 | Maxime Dénès | 2017-03-24 |
|\| | |||
| * | Merge PR#489: [travis] Add VST | Maxime Dénès | 2017-03-24 |
| |\ | |||
| | * | [travis] Add VST | Emilio Jesus Gallego Arias | 2017-03-24 |
| * | | Merge PR#392: strengthened the statement of JMeq_eq_dep | Maxime Dénès | 2017-03-24 |
| |\ \ | |||
| * \ \ | Merge branch 'v8.6' into trunk | Maxime Dénès | 2017-03-24 |
| |\ \ \ | |||
| | * \ \ | Merge PR#476: [future] Be eager when "chaining" already resolved future values. | Maxime Dénès | 2017-03-24 |
| | |\ \ \ | |||
| | * \ \ \ | Merge PR#475: Opaque side effects | Maxime Dénès | 2017-03-24 |
| | |\ \ \ \ | |||
| * | \ \ \ \ | Merge PR#504: [META] add support for ide libraries | Maxime Dénès | 2017-03-24 |
| |\ \ \ \ \ \ | |||
| * \ \ \ \ \ \ | Merge PR#503: make check not CoqIDE-specific | Maxime Dénès | 2017-03-23 |
| |\ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ | Merge PR#433: doc: fix a French-ism | Maxime Dénès | 2017-03-23 |
| |\ \ \ \ \ \ \ \ | | |_|_|_|_|_|_|/ | |/| | | | | | | | |||
| * | | | | | | | | Merge branch 'v8.6' into trunk | Maxime Dénès | 2017-03-23 |
| |\ \ \ \ \ \ \ \ | | | |_|_|/ / / / | | |/| | | | | | | |||
| | * | | | | | | | Merge PR#507: Intern names bound in match patterns | Maxime Dénès | 2017-03-23 |
| | |\ \ \ \ \ \ \ | |||
| | | | | | | * | | | Documenting the API of side-effects. | Pierre-Marie Pédrot | 2017-03-23 |
| | | | | | | * | | | Using a dedicated datastructure for side effect ordering. | Pierre-Marie Pédrot | 2017-03-23 |
| | | | | | | * | | | Making the side_effects type opaque. | Pierre-Marie Pédrot | 2017-03-23 |
| | | |_|_|_|/ / / | | |/| | | | | | | |||
| | | * | | | | | | Intern names bound in match patterns | Tej Chajed | 2017-03-23 |
| * | | | | | | | | Merge PR#501: [travis] Fix iris-coq build. | Maxime Dénès | 2017-03-23 |
| |\ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ | Merge branch 'v8.6' into trunk | Maxime Dénès | 2017-03-23 |
| |\ \ \ \ \ \ \ \ \ | | | |/ / / / / / / | | |/| | | | | | | | |||
| | * | | | | | | | | Merge PR#497: [travis] [8.6.only] Backport latest changes from trunk. | Maxime Dénès | 2017-03-23 |
| | |\ \ \ \ \ \ \ \ | |||
| * | | | | | | | | | | Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220." | Maxime Dénès | 2017-03-23 |
| * | | | | | | | | | | Merge branch 'v8.6' into trunk | Maxime Dénès | 2017-03-23 |
| |\| | | | | | | | | | |||
| | * | | | | | | | | | Merge PR#495: funind: Ignore missing info for current function | Maxime Dénès | 2017-03-23 |
| | |\ \ \ \ \ \ \ \ \ | | | |_|_|/ / / / / / | | |/| | | | | | | | | |||
| | * | | | | | | | | | Add empty Extraction.v and FunInd.v to prepare landing of PR#220. | Maxime Dénès | 2017-03-23 |
| | * | | | | | | | | | Merge PR#491: Do not typecheck twice the type of opaque constants. | Maxime Dénès | 2017-03-23 |
| | |\ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | * | | | [META] add support for ide libraries | Emilio Jesus Gallego Arias | 2017-03-23 |
| | * | | | | | | | | | | Merge PR#480: show unused intro pattern warning | Maxime Dénès | 2017-03-22 |
| | |\ \ \ \ \ \ \ \ \ \ | |||
| * | \ \ \ \ \ \ \ \ \ \ | Merge PR#493: [safe-string] update dev/doc/changes | Maxime Dénès | 2017-03-22 |
| |\ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#415: Use a compact representation for real literals | Maxime Dénès | 2017-03-22 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | | * | | | | make check not CoqIDE-specific | Paul Steckler | 2017-03-22 |
| | | | | | | | | | | |/ / / | |||
| * | | | | | | | | | / / / | Better compatibility of TACTIC EXTEND AT LEVEL with versions of camlp5. | Hugo Herbelin | 2017-03-22 |
| | |_|_|_|_|_|_|_|_|/ / / | |/| | | | | | | | | | | | |||
| | | | | | | | | * | | | | [travis] Fix iris-coq build. | Emilio Jesus Gallego Arias | 2017-03-22 |
| | |_|_|_|_|_|_|/ / / / | |/| | | | | | | | | | | |||
| | * | | | | | | | | | | Document the changes to IZR. | Guillaume Melquiond | 2017-03-22 |
| | * | | | | | | | | | | Make IZR a morphism for field. | Guillaume Melquiond | 2017-03-22 |
| | * | | | | | | | | | | Mark ring morphisms as opaque. | Guillaume Melquiond | 2017-03-22 |
| | * | | | | | | | | | | Change the parser and printer so that they use IZR for real constants. | Guillaume Melquiond | 2017-03-22 |
| | | | | | | | * | | | | [travis] [8.6.only] Backport latest changes from trunk. | Emilio Jesus Gallego Arias | 2017-03-22 |
| | | | | |_|_|/ / / / | | | | |/| | | | | | | |||
| | * | | | | | | | | | Make IZR use a compact representation of integers. | Guillaume Melquiond | 2017-03-22 |