aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-06-26Merge PR#756: Fix Bug #5574, document function scopeMaxime Dénès
2017-06-23Merge PR#813: Fix plugin warningsMaxime Dénès
2017-06-23Fix Bug #5574, document function scopePaul Steckler
2017-06-23[configure] 'ocaml' is more precise than OCaml as we mean the binary.Maxime Dénès
2017-06-23ocaml -> OCaml in configure.ml.Maxime Dénès
2017-06-23Merge PR#729: Fixing an inconsistency between configure and configure.mlMaxime Dénès
2017-06-23Merge PR#740: Refactor documentation of records.Maxime Dénès
2017-06-23Add tests for handling of warningsTej Chajed
2017-06-23Fix bug 5392: Warnings defined in plugins are considered unknownMaxime Dénès
2017-06-20Merge PR#812: Use more neutral wording instead of mentioning CoqIDEMaxime Dénès
2017-06-19Merge PR#792: Fix ci-fiat-crypto to have a proper lite targetMaxime Dénès
2017-06-19Change CoqIDE-specific to neutral wordingPaul Steckler
2017-06-16Remove -j ${NJOBS} from make invocations in the ciJason Gross
2017-06-16Pass GNU Make jobserver on to the ci jobsJason Gross
2017-06-16Fix ci-fiat-crypto to have a proper lite targetJason Gross
2017-06-16Merge PR#730: Protecting from warnings while compiling 8.6Maxime Dénès
2017-06-16Refactor documentation of records.Théo Zimmermann
2017-06-16Merge PR#767: Document named evars (including Show ident)Maxime Dénès
2017-06-15Merge PR#741: Fix documentation of Typeclasses eauto :=Maxime Dénès
2017-06-15Merge PR#713: Bump year in headers.Maxime Dénès
2017-06-15Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraintsMaxime Dénès
2017-06-15Merge PR#752: Adding a test case as requested in bug 5205.Maxime Dénès
2017-06-15Merge PR#747: Fix Bug #5568, no dup notation warnings on repeated module importsMaxime Dénès
2017-06-13Document instantiate (ident := term) and make it the preferred variant.Théo Zimmermann
2017-06-13Document Show ident.Théo Zimmermann
2017-06-13Document evar naming syntax.Théo Zimmermann
2017-06-09Fix Bug #5568, no dup notation warnings on repeated module importsPaul Steckler
2017-06-08Adding a test case as requested in bug 5205.Théo Zimmermann
2017-06-07Fix documentation of Typeclasses eauto :=Théo Zimmermann
2017-06-05Univs: fix bug #5365, generation of u+k <= v constraintsMatthieu Sozeau
2017-06-04Ensure that warnings new from ocaml > 4.01 remains silent.Hugo Herbelin
2017-06-04configure: avoid deprecated warningsPierre Letouzey
2017-06-04Fixing an inconsistency between configure and configure.ml.Hugo Herbelin
2017-06-02Merge PR#705: Fix bug #5019 (looping zify on dependent types)Maxime Dénès
2017-06-01Merge PR#631: Fix bug #5255Maxime Dénès
2017-06-01Bump year in headers.Maxime Dénès
2017-06-01Fix bug #5019 (looping zify on dependent types)Jason Gross
2017-06-01Add opened bug 5019Jason Gross
2017-06-01Merge PR#710: Add test-suite checks for coqchk with constraintsMaxime Dénès
2017-05-31Merge PR#560: Reinstate fixpoint refolding in [cbn], deactivated by mistake (...Maxime Dénès
2017-05-31Merge PR#699: Fix bug 5550: "typeclasses eauto with" does not work with secti...Maxime Dénès
2017-05-30Add test-suite checks for coqchk with constraintsJason Gross
2017-05-30Merge PR#693: A subtle bug in tclWITHHOLES.Maxime Dénès
2017-05-30Merge PR#695: Omega: fix bug #4132Maxime Dénès
2017-05-30Fix bug 5550: "typeclasses eauto with" does not work with section variables.Théo Zimmermann
2017-05-29Omega: use "simpl" only on coefficents, not on atoms (fix #4132)Pierre Letouzey
2017-05-29Merge PR#685: Fix a bug in checkerMaxime Dénès
2017-05-29Merge PR#546: Fix for bug #4499 and other minor related bugsMaxime Dénès
2017-05-28Fix a bug in checkerAmin Timany
2017-05-28Fixing a subtle bug in tclWITHHOLES.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 14:32:05 +0000