aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-01-22Move the mention of the removal of Qed exporting at the right place.Théo Zimmermann
2018-01-22Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.Maxime Dénès
2018-01-22Merge PR #6625: Update location on tab switch, issue 6624Maxime Dénès
2018-01-22Merge PR #6576: generate both binary and text annotationsMaxime Dénès
2018-01-22Merge PR #6550: Remove outdated note about rlwrap in setup.txtMaxime Dénès
2018-01-22Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints.Maxime Dénès
2018-01-22Merge PR #6575: Add flash infos for find and replaceMaxime Dénès
2018-01-22Merge PR #6506: Fast rel lookupMaxime Dénès
2018-01-22[printing] Remove duplicate definitions of pr_lident and pr_lnameVincent Laporte
2018-01-20Adding a test for coqchk bug #6619.Pierre-Marie Pédrot
2018-01-20Fix #6618: coqchk fails with "ill-typed term".Pierre-Marie Pédrot
2018-01-20Remove dead code in Environ.Pierre-Marie Pédrot
2018-01-19-annotate deprecated. New options: -annot, -bin-annotVadim Zaliva
2018-01-19update location on tab switch, issue 6624Paul Steckler
2018-01-19Add test-suite file for issue #6617.Cyprien Mangin
2018-01-19Fix context handling of fix and cofix in Ltac subterm matching.Cyprien Mangin
2018-01-19Define EConstr version of [push_rec_types].Cyprien Mangin
2018-01-18add flash infos about wrap, not found, no. of replacements, no. of finds, iss...Paul Steckler
2018-01-18Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.Maxime Dénès
2018-01-18Merge PR #6448: Cleanup and add debug printers a bitMaxime Dénès
2018-01-17Merge PR #6600: Update configure.ml to only warn on lablgtk >= 2.16.0 and < 2...Maxime Dénès
2018-01-17Merge PR #6593: Add plugins to META.coqMaxime Dénès
2018-01-17Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop)Maxime Dénès
2018-01-17Merge PR #6584: Implement the strategy mechanism in the checkerMaxime Dénès
2018-01-17Add CHANGES entryJasper Hugunin
2018-01-17Let dtauto recognize '@sigT A (fun _ => B)' as a conjunctionJasper Hugunin
2018-01-17Add CHANGES entryJasper Hugunin
2018-01-17Add a test that `prod_applist_assum` reduces the right number of let-insJasper Hugunin
2018-01-17Use let-in aware prod_applist_assum in dtauto and firstorder.Jasper Hugunin
2018-01-16Update lablgtk check to be more generalJason Gross
2018-01-16Rename coq.ltac to coq.plugins.ltac in META.coqCyprien Mangin
2018-01-16Update configure.ml to only warn on lablgtk 2.16.0Jason Gross
2018-01-16merge-pr.sh: use git diff --quietGaëtan Gilbert
2018-01-16Source basic overlay before user overlays.Gaëtan Gilbert
2018-01-16Cleanup shell expansions and quoting.Gaëtan Gilbert
2018-01-16Simplify logic and streamline lint-repository.shGaëtan Gilbert
2018-01-16Merge PR #6590: Fix the wrapper around ocamldebug.Maxime Dénès
2018-01-16Merge PR #6499: [vernac] Move the flags/attributes out of vernac_exprMaxime Dénès
2018-01-16Merge PR #6466: Replace md5sum/md5 calls by an OCaml programMaxime Dénès
2018-01-16Merge PR #6551: Bracket with goal selectorMaxime Dénès
2018-01-16Add plugins to META.coqCyprien Mangin
2018-01-15Fix the wrapper around ocamldebug.Pierre-Marie Pédrot
2018-01-15Avoid shell backticks and improve md5sum.ml error messagesJacques-Pascal Deplaix
2018-01-15More tests on brackets with goal selectors (including failures).Théo Zimmermann
2018-01-15Add test-suite file for bracket with goal selector.Théo Zimmermann
2018-01-14Actually use the strategy information in the checker.Pierre-Marie Pédrot
2018-01-14Store the conversion oracle in constant and inductive definitions.Pierre-Marie Pédrot
2018-01-13Merge PR #6578: Remove references to deleted Unicode.Unsupported exceptionMaxime Dénès
2018-01-13Merge PR #6581: Added newline at the end of usage of coqdep.Maxime Dénès
2018-01-13Merge PR #6564: Fix undefined variables in test-suite/Makefile + add PRINT_LOGSMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-24 13:20:14 +0000