| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-08-25 | Renaming the bindings scope into with_bindings. | Pierre-Marie Pédrot | |
| 2017-08-25 | Do not return STRING scopes in the tuple produced by "seq" scopes. | Pierre-Marie Pédrot | |
| 2017-08-25 | More bindings to primitive tactics. | Pierre-Marie Pédrot | |
| 2017-08-25 | Respect the default goal selector in toplevel invocations. | Pierre-Marie Pédrot | |
| 2017-08-25 | Parse specifically idents as destruction arguments. | Pierre-Marie Pédrot | |
| This is for backward compatibility. | |||
| 2017-08-25 | Lookahead to cheat the constr parser in order to parse "& IDENT". | Pierre-Marie Pédrot | |
| 2017-08-25 | primproj: fix bug 5245, hnf on proj with simpl never flag. | Matthieu Sozeau | |
| 2017-08-24 | Don't strip the newline, don't use \r | Jason Gross | |
| Not sure entirely what it was supposed to do, but stripping the newline erased the following line | |||
| 2017-08-24 | Swap order of "aggregating..." message and travis_fold | Jason Gross | |
| Now the folded line starts with "Aggregating..." and not with "---------" | |||
| 2017-08-24 | [ci] [gitlab] coq-dpdgraph: Remove allow-failure | Jason Gross | |
| 2017-08-24 | Only display travis_fold: on travis | Jason Gross | |
| 2017-08-24 | Fix the semantics of fail, as it should enter the goal. | Pierre-Marie Pédrot | |
| 2017-08-24 | Documentation about the transition from Ltac1. | Pierre-Marie Pédrot | |
| 2017-08-24 | Removing dead code about arrays in the AST. | Pierre-Marie Pédrot | |
| 2017-08-24 | Rely on quoting for lists instead of hardwiring it in the AST. | Pierre-Marie Pédrot | |
| 2017-08-24 | Program: fix BZ#5683, missing lift when building case predicate | Matthieu Sozeau | |
| 2017-08-24 | Adding a notation for the unfold tactic. | Pierre-Marie Pédrot | |
| 2017-08-24 | Adding a notation scope for global references. | Pierre-Marie Pédrot | |
| 2017-08-24 | Adding notation for the remaining reduction functions. | Pierre-Marie Pédrot | |
| 2017-08-24 | Fix typing of reference quotations. | Pierre-Marie Pédrot | |
| 2017-08-24 | Adding a scope for reduction flags. | Pierre-Marie Pédrot | |
| 2017-08-24 | Introducing a quotation for global references. | Pierre-Marie Pédrot | |
| 2017-08-24 | Use references in reduction tactics. | Pierre-Marie Pédrot | |
| We dynamically check that the provided references are indeed evaluable ones, instead of ensuring this at internalization time. | |||
| 2017-08-24 | Update .mailmap file. | Guillaume Melquiond | |
| 2017-08-23 | Update coypright dates on documentation | Matthieu Sozeau | |
| 2017-08-23 | Fix BZ#5687: Coqtop died badly modal message box from CoqIDE. | Pierre-Marie Pédrot | |
| We let the user choose the most appropriate action to do if coqtop decides to go berserk. | |||
| 2017-08-22 | use OCaml 4.03-compatible Filename functions | Paul Steckler | |
| 2017-08-22 | also in Fun1.smartmap, read, write from same array | Paul Steckler | |
| 2017-08-22 | Prevent warning about DSTROOT being undefined. | Guillaume Melquiond | |
| 2017-08-22 | Prevent overallocation in Array.map_to_list and remove custom implementation ↵ | Guillaume Melquiond | |
| from Detyping. | |||
| 2017-08-22 | Fix obsolete description of real numerals. | Guillaume Melquiond | |
| 2017-08-21 | read, write from same array | Paul Steckler | |
| 2017-08-21 | Ensuring all .v files end with a newline to make "sed -i" work better on them. | Hugo Herbelin | |
| 2017-08-21 | Fix coqdoc URLs under Windows. | Théo Zimmermann | |
| URLs on Windows are the same as on Unix, they use / not \. | |||
| 2017-08-21 | Extend .gitignore for coqdoc test-suite. | Théo Zimmermann | |
| 2017-08-21 | Fix coqdoc test-suite target on Windows. | Théo Zimmermann | |
| Commit 8f12597 introduced new output tests but these were broken on Windows. We fix them by using --strip-trailing-cr option of diff, like in other output tests in the test-suite. | |||
| 2017-08-21 | Fixing another regression with 8.4 wrt to βι-normalization of created hyps. | Hugo Herbelin | |
| This one is a continuation of e2a8edaf59 which was βι-normalizing the hypotheses created by a "match". We forgot to do it for "let" and "if". This is what this commit is doing. | |||
| 2017-08-21 | Fixing a new regresssion with 8.4 wrt to βι-normalization of created hyps. | Hugo Herbelin | |
| Formerly, mk_refgoals in logic.ml was applying full βι on new Meta-based goals. We simulate part of this βι-normalization in pose_all_metas_as_evars. I suspect that we don't βι-normalize goals more than in 8.4 by doing that, since all Metas would have eventually gone to mk_refgoals, but difficult to know for sure as there were probably metas turned to evars (and hence a priori not βι-normalized) even when logic.ml was used more pervasively. However, βι-normalizing is a priori a better heuristic than no βι-normalizing, independently of what it was in 8.4 and before (even if, ideally, I would personally lean towards preferring a "chirurgical" substitution with reduction only at the place of substitution). | |||
| 2017-08-18 | use OCaml temp_file, instead of our own version | Paul Steckler | |
| 2017-08-18 | add CHANGES entry | Paul Steckler | |
| 2017-08-18 | move filename search to start_profiler | Paul Steckler | |
| 2017-08-18 | Merge PR #965: Moving file primitive.ml to cPrimitive.ml to avoid conflict ↵ | Maxime Dénès | |
| with OCaml. | |||
| 2017-08-18 | More precise type for quotation entries. | Pierre-Marie Pédrot | |
| 2017-08-18 | Removing dead code. | Pierre-Marie Pédrot | |
| 2017-08-18 | Laxer dependencies between file and link reordering. | Pierre-Marie Pédrot | |
| 2017-08-18 | Notations for a few reduction functions. | Pierre-Marie Pédrot | |
| 2017-08-18 | Merge PR #983: Correct the option for cumulativity in CHANGES | Maxime Dénès | |
| 2017-08-18 | Merge PR #973: Adding documentation for Printing Focused option. | Maxime Dénès | |
| 2017-08-18 | Correct the option for cumulativity in CHANGES | Amin Timany | |
| 2017-08-18 | Merge PR #801: Make Travis generate OSX packages. | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |