| Commit message (Expand) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| | * | | | | | | Passing chan_beautify functionally rather than by side-effect. |  Hugo Herbelin | 2016-10-17 | |
| | * | | | | | | Applying Emilio's suggestion to simplify type of eval_expr. | Hugo Herbelin | 2016-10-17 | |
| | * | | | | | | More on making the lexer more functional (continuing b8ae2de5 and | Hugo Herbelin | 2016-10-17 | |
| | * | | | | | | Removing export of location_table outside of cLexer. | Hugo Herbelin | 2016-10-17 | |
| | * | | | | | | Fix compilation with camlp4 broken in 8a8caba3. | Hugo Herbelin | 2016-10-17 | |
| | | * | | | | | Fixing to #3209 (Not_found due to an occur-check cycle). | Hugo Herbelin | 2016-10-17 | |
| | | * | | | | | Fixing a missing constraint in consider_remaining_unif_constraints. | Hugo Herbelin | 2016-10-17 | |
| * | | | | | | | Merge branch 'v8.6' |  Pierre-Marie Pédrot | 2016-10-17 | |
| |\| | | | | | | ||||
| | * | | | | | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-10-17 | |
| | |\| | | | | | ||||
| | * | | | | | | Fix output test for module qualification. | Pierre-Marie Pédrot | 2016-10-17 | |
| | * | | | | | | Fix previous commit. | Pierre-Marie Pédrot | 2016-10-17 | |
| | * | | | | | | Merge PR #300 into v8.6 | Pierre-Marie Pédrot | 2016-10-17 | |
| | |\ \ \ \ \ \ | ||||
| | * | | | | | | | Example illustrating non-local inference of the default type of impossible br... | Hugo Herbelin | 2016-10-17 | |
| | | | * | | | | | Merge PR #310 into v8.5 | Pierre-Marie Pédrot | 2016-10-17 | |
| | | | |\ \ \ \ \ | ||||
| | * | | \ \ \ \ \ | Merge PR #310 into v8.6 | Pierre-Marie Pédrot | 2016-10-17 | |
| | |\ \ \ \ \ \ \ \ | | | |_|/ / / / / | | |/| | | | | | | ||||
| | | * | | | | | | | Test for bug #4874. | Pierre-Marie Pédrot | 2016-10-17 | |
| | * | | | | | | | | Fix bug #5023: JSON extraction doesn't generate "for xxx". | Pierre-Marie Pédrot | 2016-10-17 | |
| | * | | | | | | | | Fix bug #5141: Bogus message "Error: Cannot infer type of pattern-matching". | Pierre-Marie Pédrot | 2016-10-16 | |
| | * | | | | | | | | Fix bug #5145: Anomaly: index to an anonymous variable. | Pierre-Marie Pédrot | 2016-10-15 | |
| | | |_|_|_|_|/ / | |/| | | | | | | ||||
| | | | | * | | | | Still a problem with debug auto printing. | Hugo Herbelin | 2016-10-15 | |
| | | | | * | | | | One more little bug in the output of "debug auto". | Hugo Herbelin | 2016-10-15 | |
| | * | | | | | | | Fix bug #5139: Anomalies should not be caught by || / try. | Pierre-Marie Pédrot | 2016-10-14 | |
| | | | | * | | | | Fixing printing of info_auto broken since 0091c528 (2014). | Hugo Herbelin | 2016-10-14 | |
| | * | | | | | | | Fixing English typography for colon. | Hugo Herbelin | 2016-10-14 | |
| | * | | | | | | | Using "simple apply" and "simple eapply" in the trace of auto. | Hugo Herbelin | 2016-10-14 | |
| | * | | | | | | | Completing reverting generalization and cleaning of the return clause inference. | Hugo Herbelin | 2016-10-13 | |
| | * | | | | | | | Remove dead code in Environ. | Pierre-Marie Pédrot | 2016-10-12 | |
| | * | | | | | | | Merge PR #224 into v8.6 | Pierre-Marie Pédrot | 2016-10-12 | |
| | |\ \ \ \ \ \ \ | ||||
| | * \ \ \ \ \ \ \ | Merge PR #289 into v8.6. | Pierre-Marie Pédrot | 2016-10-12 | |
| | |\ \ \ \ \ \ \ \ | ||||
| * | | | | | | | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-10-12 | |
| |\| | | | | | | | | | ||||
| | * | | | | | | | | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-10-12 | |
| | |\ \ \ \ \ \ \ \ \ | | | |_|_|_|/ / / / | | |/| | | | | | | | ||||
| | * | | | | | | | | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-10-12 | |
| | |\ \ \ \ \ \ \ \ \ | ||||
| * | | | | | | | | | | | Allocating a section in CHANGES for changes specific to 8.7. | Hugo Herbelin | 2016-10-12 | |
| | * | | | | | | | | | | Tentatively preparing to add changes specific to v8.7 (see PR #275). | Hugo Herbelin | 2016-10-12 | |
| | * | | | | | | | | | | Little addition to 6eede071 for consistency of style in OrdersFacts.v. | Hugo Herbelin | 2016-10-12 | |
| | | | * | | | | | | | | Fixing a collision about the meta-variable ".." in recursive notations. | Hugo Herbelin | 2016-10-12 | |
| | | | * | | | | | | | | Merge remote-tracking branch 'github/pr/286' into v8.5 |  Maxime Dénès | 2016-10-12 | |
| | | | |\ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | | | | | Fix bug #5116: [Print Ltac] should be able to print strategies. | Pierre-Marie Pédrot | 2016-10-12 | |
| | * | | | | | | | | | | | Fix git recognition when in worktrees. |  Théo Zimmermann | 2016-10-12 | |
| | * | | | | | | | | | | | Fix bug #4958: [debug auto] should specify hint databases. | Pierre-Marie Pédrot | 2016-10-12 | |
| | * | | | | | | | | | | | Shorter message for "Test Asymmetric Patterns". | Hugo Herbelin | 2016-10-12 | |
| | | | * | | | | | | | | | Merge remote-tracking branch 'git/bug5123' into v8.5 |  Matthieu Sozeau | 2016-10-12 | |
| | | |/| | | | | | | | | | ||||
| | * | | | | | | | | | | | Fixing a few confusions on the name of the beautify flag. | Hugo Herbelin | 2016-10-12 | |
| | | | * | | | | | | | | | Fix test-suite file 5123 to fail in case of regression |  Matthieu Sozeau | 2016-10-11 | |
| | | * | | | | | | | | | | Merge remote-tracking branch 'github/bug4863' into v8.5 | Matthieu Sozeau | 2016-10-11 | |
| | | |\ \ \ \ \ \ \ \ \ \ | ||||
| | | | | * | | | | | | | | | Fix bug #5123: mark all shelved evars unresolvable | Matthieu Sozeau | 2016-10-11 | |
| | | | |/ / / / / / / / / | | |/| | | | | | | | | | ||||
| | * | | | | | | | | | | | Reverting generalization and cleaning of the return clause inference in v8.6. | Hugo Herbelin | 2016-10-11 | |
| | | | * | | | | | | | | | Fix for bug #4863, update the Proofview's env with | Matthieu Sozeau | 2016-10-11 | |
| | | |/ / / / / / / / / | ||||
| | * | | | | | | | | | | Fixing #5133 (error reporting delayed). | Hugo Herbelin | 2016-10-10 | |
| | | * | | | | | | | | | Add test file for #4416. | Maxime Dénès | 2016-10-10 | |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |