aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
2019-05-24Fixing typosJPR
2019-05-23Fixing typos - Part 3JPR
2019-05-15Merge PR #10151: Clean up the API for side-effectsGaëtan Gilbert
2019-05-14Merge PR #8893: Moving evars_of_term from constr to econstrPierre-Marie Pédrot
2019-05-14Abstract away the implementation of side-effects in Safe_typing.Pierre-Marie Pédrot
2019-05-14Allow run_tactic to return a value, remove hack from ltac2Gaëtan Gilbert
2019-05-13Passing evar_map to evars_of_term rather than expecting the term to be evar-nf.Hugo Herbelin
2019-05-13Merge PR #9887: [api] Remove 8.10 deprecations.Gaëtan Gilbert
2019-05-10Fast-path for reordering of a single closed variable.Pierre-Marie Pédrot
2019-05-10Split the hypothesis conversion check in a conversion + ordering check.Pierre-Marie Pédrot
2019-05-10Logic.convert_hyp now takes an environment as an argument.Pierre-Marie Pédrot
2019-05-10Cleanup of Logic.convert_hyp.Pierre-Marie Pédrot
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2019-04-24Fix proof bullet error helper (nosuchgoal)Gaëtan Gilbert
2019-04-24[proof] Fix proof bullet error helper which was implemented as a hookEmilio Jesus Gallego Arias
2019-04-05[api] [proofs] Remove dependency of proofs on interp.Emilio Jesus Gallego Arias
2019-04-02Merge PR #9659: Fix #9652: rewrite fails to detect lack of progressEmilio Jesus Gallego Arias
2019-03-27[geninterp] Track polymorphic status in tactic interpretation.Emilio Jesus Gallego Arias
2019-03-27[proof_global] Removal of imperative state.Emilio Jesus Gallego Arias
2019-03-25Fix #9652: rewrite fails to detect lack of progressGaëtan Gilbert
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-12Merge PR #7819: Ho matching occ selEnrico Tassi
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-12[tactics] Remove dependency of abstract on global proof state.Emilio Jesus Gallego Arias
2019-02-08Fix indentation (removing tabs)Matthieu Sozeau
2019-02-08[evarconv] New flag handling for unifierMatthieu Sozeau
2019-02-08Evd/evarsolve: add an abstraction field to evars for unificationMatthieu Sozeau
2019-02-05Make Program a regular attributeMaxime Dénès
2019-02-01Fix default goal selector error message.Gaëtan Gilbert
2019-01-24[STM] explicit handling of parsing statesEnrico Tassi
2019-01-21At Qed, if shelved goals remain, emit a warning instead of an errorMaxime Dénès
2018-12-19Merge PR #9139: [engine] Allow debug printers to access the environment.Pierre-Marie Pédrot
2018-12-18Merge PR #9223: Fix universe restriction in delayed mode.Pierre-Marie Pédrot
2018-12-18Merge PR #9222: Fix classification of Set Default Proof Mode.Enrico Tassi
2018-12-17Merge PR #9153: [api] Move reduction modules to `tactics`Pierre-Marie Pédrot
2018-12-17Restrict body universes in delayed mode.Gaëtan Gilbert
2018-12-17Fix classification of Set Default Proof Mode.Gaëtan Gilbert
2018-12-17Merge PR #9220: Move shallow state logic to the function preparing state for ...Enrico Tassi
2018-12-14[proof] Rework proof interface.Emilio Jesus Gallego Arias
2018-12-13[engine] Allow debug printers to access the environment.Emilio Jesus Gallego Arias
2018-12-13Move shallow state logic to the function preparing state for workersMaxime Dénès
2018-12-12Merge PR #8965: Add `String Notation` vernacular like `Numeral Notation`Hugo Herbelin
2018-12-11[api] Move reduction modules to `tactics`Emilio Jesus Gallego Arias
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-12-04Remove undocumented "Proof using Clear Unused" flagJim Fehrle
2018-11-28Factor out common code in numeral/string notationsJason Gross
2018-11-27Merge PR #9046: Goptions.declare_* functions return unit instead of a write_f...Emilio Jesus Gallego Arias
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
2018-11-23s/let _ =/let () =/ in some places (mostly goptions related)Gaëtan Gilbert
2018-11-22Merge PR #8967: Fix #8922 (uncaught pp_diff exception)Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:45:25 +0000