aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-05-03Remove a call to V82.tactic in Btauto.Pierre-Marie Pédrot
2020-05-03Remove a very specific low-level tactical from Refiner.Pierre-Marie Pédrot
2020-05-03Wrap Refiner.refiner in the tactic monad.Pierre-Marie Pédrot
2020-05-03Remove a critical call to V82.tactic in Clenvtac.Pierre-Marie Pédrot
2020-05-03consistency with PermutationOlivier Laurent
2020-05-03Simplify division of Cauchy realsVincent Semeria
2020-05-03Ensure eintros allows creating evarsPaolo G. Giarrusso
2020-05-02Fix #12159 (Numeral Notations do not play well with multiple scopes for the s...Pierre Roux
2020-05-02Merge PR #12172: Refactor first chapter: first step, the section on basics.Clément Pit-Claudel
2020-05-02Move tclWRAPFINALLY to profile_ltacJason Gross
2020-05-02Decrease LtacProf overhead when not profilingJason Gross
2020-05-02LtacProf now handles multi-success backtrackingJason Gross
2020-05-02Add Proofview.tclWRAPFINALLYJason Gross
2020-05-02Adding change logs for PR #12121.Hugo Herbelin
2020-05-01Testing different combinations of non truly recursive (co)fixpoints.Hugo Herbelin
2020-05-01Changing fixpoint message "decreasing" -> "guarded".Hugo Herbelin
2020-05-01Fixing #11903: Fixpoints not truly recursive in standard library.Hugo Herbelin
2020-05-01Warn when a (co)fixpoint is not truly recursive.Hugo Herbelin
2020-05-01Slight modification of the partial-order algorithm so that it does notHugo Herbelin
2020-05-01Move essential vocabulary and syntax conventions to section on basics.Théo Zimmermann
2020-05-01Merge PR #12221: Replace QSeqEquiv by QCauchySeq, simplify proofs.Michael Soegtrop
2020-05-01Preserve vernac chapter.Théo Zimmermann
2020-05-01Extract two new files out of Gallina chapter.Théo Zimmermann
2020-05-01Create section on writing libraries with only deprecated attributes.Théo Zimmermann
2020-05-01Extract deprecated attribute from Gallina chapter.Théo Zimmermann
2020-05-01Remove flags, options and tables from vernac chapter.Théo Zimmermann
2020-05-01Remove lexical conventions and attributes from Gallina chapter.Théo Zimmermann
2020-05-01Create basics out of sections from Gallina and Vernac chapters.Théo Zimmermann
2020-05-01Create section on basics with just flags, options and tables.Théo Zimmermann
2020-05-01Extract flags, options and tables from vernac chapter.Théo Zimmermann
2020-05-01Create section on basics with just lexical conventions and attributes.Théo Zimmermann
2020-05-01Extract lexical conventions and attributes from Gallina chapter.Théo Zimmermann
2020-05-01Merge PR #12217: Fix #12215: ci scripts naming inconsistenciesEmilio Jesus Gallego Arias
2020-05-01Merge PR #12222: Less confusing configure message when lablgtk exists but not...Emilio Jesus Gallego Arias
2020-05-01do not re-export ListNotations from Program: vst overlayAntonio Nikishaev
2020-04-30Replace QSeqEquiv by QCauchySeq, simplify proofs.Vincent Semeria
2020-04-30Less confusing configure message when lablgtk exists but not lablgtksourceview.Hugo Herbelin
2020-04-30Merge PR #12213: [zify] add support for Nat.le, Nat.lt and Nat.eqVincent Laporte
2020-04-30renaming in Makefile.ci and ci scripts to avoid inconsistenciesOlivier Laurent
2020-04-30Merge PR #12216: Remove outdated code and comments in Declare.Emilio Jesus Gallego Arias
2020-04-30Move availability_of_prim_tokenPierre Roux
2020-04-30[zify] add support for Nat.le, Nat.lt and Nat.eqFrédéric Besson
2020-04-30Merge PR #12107: Remove mod_constraints field of module bodyPierre-Marie Pédrot
2020-04-30Remove outdated code and comments in Declare.Pierre-Marie Pédrot
2020-04-30Symmetry in conclusions of List.map_eq_*Olivier Laurent
2020-04-30Merge PR #12208: Reduce rational numbers in Cauchy real addition, to accelera...Michael Soegtrop
2020-04-30do not re-export ListNotations from Program: fix testsuiteAntonio Nikishaev
2020-04-30do not re-export ListNotations from Program: changelogAntonio Nikishaev
2020-04-30do not re-export ListNotations from Program: overlaysAntonio Nikishaev
2020-04-30do not re-export ListNotations from ProgramAntonio Nikishaev
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 15:42:14 +0000