aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-05-04strenghten nth_extOlivier Laurent
2020-05-04add incl_map incl_filter NoDup_filterOlivier Laurent
2020-05-03Merge PR #12231: Simplify division of Cauchy realsMichael Soegtrop
2020-05-03Merge PR #12238: [stdlib] [CPermutation] patch for #12031Hugo Herbelin
2020-05-03[declare] Add deprecation notices for compat modules.Emilio Jesus Gallego Arias
2020-05-03[funind] Remove use of low-level entries in scheme generation.Emilio Jesus Gallego Arias
2020-05-03[funind] Make `build_functional_principle` use a functional evar_mapEmilio Jesus Gallego Arias
2020-05-03Merge PR #12197: LtacProf now handles multi-success backtrackingPierre-Marie Pédrot
2020-05-03Add tests uncovered during bug chasing in the CI.Pierre-Marie Pédrot
2020-05-03Add overlays.Pierre-Marie Pédrot
2020-05-03Further port of ssr tacticsPierre-Marie Pédrot
2020-05-03Further port of SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Remove legacy API in SSR.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tacticsPierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further SSR port.Pierre-Marie Pédrot
2020-05-03Remove legacy SSR API.Pierre-Marie Pédrot
2020-05-03Further SSR port.Pierre-Marie Pédrot
2020-05-03Remove legacy layer in SSR.Pierre-Marie Pédrot
2020-05-03Further port of SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR code.Pierre-Marie Pédrot
2020-05-03Export new combinators in SSR not relying on the legacy API.Pierre-Marie Pédrot
2020-05-03Further porting of ssrcode.Pierre-Marie Pédrot
2020-05-03Slightly more tricky port of the ssr tactics.Pierre-Marie Pédrot
2020-05-03Export missing tacticals.Pierre-Marie Pédrot
2020-05-03Further port SSReflect tactics to the new engine.Pierre-Marie Pédrot
2020-05-03Wrap ssr tactics into V82.tactic.Pierre-Marie Pédrot
2020-05-03Wrap a monadic combinator in a try-with block to catch exceptions.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 13:08:41 +0000