aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
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
2018-11-21[legacy proof engine] Remove some cruft.Emilio Jesus Gallego Arias
2018-11-20Merge PR #8982: [proof] Provide better control of "open proofs" exceptions.Pierre-Marie Pédrot
2018-11-20Merge PR #9002: [pfedit] Remove `start_proof` stub from `Pfedit`Pierre-Marie Pédrot
2018-11-20Merge PR #7925: Clean transparent stateMaxime Dénès
2018-11-19[pfedit] Remove `start_proof` stub from `Pfedit`Emilio Jesus Gallego Arias
2018-11-19Rename TranspState into TransparentState.Pierre-Marie Pédrot
2018-11-19Proper record type and accessors for transparent states.Pierre-Marie Pédrot
2018-11-19Move transparent_state to its own module.Pierre-Marie Pédrot
2018-11-19[proof] Provide better control of "open proofs" exceptions.Emilio Jesus Gallego Arias
2018-11-17[pfedit] Remove cook_proof stub.Emilio Jesus Gallego Arias
2018-11-16Remove the implicit tactic feature following #7229.Pierre-Marie Pédrot
2018-11-14Get hyps and goal the same way Printer does; don't omit infoJim Fehrle
2018-11-07Revert "Do not allow spliting in res_pf, this is reserved for pretyping"Enrico Tassi
2018-10-31Renaming is_template_polymorphic -> is_template_polymorphic_ind.Hugo Herbelin
2018-10-31Merge PR #8841: Share the construction of the evar instance in Clenv.make_eva...Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:21:28 +0000