aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-08-25Renaming the bindings scope into with_bindings.Pierre-Marie Pédrot
2017-08-25Do not return STRING scopes in the tuple produced by "seq" scopes.Pierre-Marie Pédrot
2017-08-25More bindings to primitive tactics.Pierre-Marie Pédrot
2017-08-25Respect the default goal selector in toplevel invocations.Pierre-Marie Pédrot
2017-08-25Parse specifically idents as destruction arguments.Pierre-Marie Pédrot
2017-08-25Lookahead to cheat the constr parser in order to parse "& IDENT".Pierre-Marie Pédrot
2017-08-25primproj: fix bug 5245, hnf on proj with simpl never flag.Matthieu Sozeau
2017-08-24Don't strip the newline, don't use \rJason Gross
2017-08-24Swap order of "aggregating..." message and travis_foldJason Gross
2017-08-24[ci] [gitlab] coq-dpdgraph: Remove allow-failureJason Gross
2017-08-24Only display travis_fold: on travisJason Gross
2017-08-24Fix the semantics of fail, as it should enter the goal.Pierre-Marie Pédrot
2017-08-24Documentation about the transition from Ltac1.Pierre-Marie Pédrot
2017-08-24Removing dead code about arrays in the AST.Pierre-Marie Pédrot
2017-08-24Rely on quoting for lists instead of hardwiring it in the AST.Pierre-Marie Pédrot
2017-08-24Program: fix BZ#5683, missing lift when building case predicateMatthieu Sozeau
2017-08-24Adding a notation for the unfold tactic.Pierre-Marie Pédrot
2017-08-24Adding a notation scope for global references.Pierre-Marie Pédrot
2017-08-24Adding notation for the remaining reduction functions.Pierre-Marie Pédrot
2017-08-24Fix typing of reference quotations.Pierre-Marie Pédrot
2017-08-24Adding a scope for reduction flags.Pierre-Marie Pédrot
2017-08-24Introducing a quotation for global references.Pierre-Marie Pédrot
2017-08-24Use references in reduction tactics.Pierre-Marie Pédrot
2017-08-24Update .mailmap file.Guillaume Melquiond
2017-08-23Update coypright dates on documentationMatthieu Sozeau
2017-08-23Fix BZ#5687: Coqtop died badly modal message box from CoqIDE.Pierre-Marie Pédrot
2017-08-22use OCaml 4.03-compatible Filename functionsPaul Steckler
2017-08-22also in Fun1.smartmap, read, write from same arrayPaul Steckler
2017-08-22Prevent warning about DSTROOT being undefined.Guillaume Melquiond
2017-08-22Prevent overallocation in Array.map_to_list and remove custom implementation ...Guillaume Melquiond
2017-08-22Fix obsolete description of real numerals.Guillaume Melquiond
2017-08-21read, write from same arrayPaul Steckler
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2017-08-21Fix coqdoc URLs under Windows.Théo Zimmermann
2017-08-21Extend .gitignore for coqdoc test-suite.Théo Zimmermann
2017-08-21Fix coqdoc test-suite target on Windows.Théo Zimmermann
2017-08-21Fixing another regression with 8.4 wrt to βι-normalization of created hyps.Hugo Herbelin
2017-08-21Fixing a new regresssion with 8.4 wrt to βι-normalization of created hyps.Hugo Herbelin
2017-08-18use OCaml temp_file, instead of our own versionPaul Steckler
2017-08-18add CHANGES entryPaul Steckler
2017-08-18move filename search to start_profilerPaul Steckler
2017-08-18Merge PR #965: Moving file primitive.ml to cPrimitive.ml to avoid conflict wi...Maxime Dénès
2017-08-18More precise type for quotation entries.Pierre-Marie Pédrot
2017-08-18Removing dead code.Pierre-Marie Pédrot
2017-08-18Laxer dependencies between file and link reordering.Pierre-Marie Pédrot
2017-08-18Notations for a few reduction functions.Pierre-Marie Pédrot
2017-08-18Merge PR #983: Correct the option for cumulativity in CHANGESMaxime Dénès
2017-08-18Merge PR #973: Adding documentation for Printing Focused option.Maxime Dénès
2017-08-18Correct the option for cumulativity in CHANGESAmin Timany
2017-08-18Merge PR #801: Make Travis generate OSX packages.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-26 11:39:21 +0000