aboutsummaryrefslogtreecommitdiff
path: root/proofs/proof_global.ml
AgeCommit message (Expand)Author
2019-06-04Proof_global: pass only 1 pstate when we don't want the proof stackGaëtan Gilbert
2019-05-14Allow run_tactic to return a value, remove hack from ltac2Gaëtan Gilbert
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-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-14Add relevance marks on binders.Gaëtan Gilbert
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-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-18Merge PR #9223: Fix universe restriction in delayed mode.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-13Move shallow state logic to the function preparing state for workersMaxime Dénès
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-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-19[proof] Provide better control of "open proofs" exceptions.Emilio Jesus Gallego Arias
2018-10-16{Univops -> Vars}.universes_of_constrGaëtan Gilbert
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
2018-06-26universes_of_constr don't include universes of monomorphic constantsGaëtan Gilbert
2018-06-12[api] Misctypes removal: miscellaneous aliases.Emilio Jesus Gallego Arias
2018-06-04[econstr] Remove some Unsafe.to_constr use.Emilio Jesus Gallego Arias
2018-05-31[api] Move `Constrexpr` to the `interp` module.Emilio Jesus Gallego Arias
2018-05-23[api] Move `opacity_flag` to `Proof_global`.Emilio Jesus Gallego Arias
2018-05-17Split off Universes functions about substitutions and constraintsGaëtan Gilbert
2018-05-01[api] Move bullets and goals selectors to `proofs/`Emilio Jesus Gallego Arias
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-03-08Cosmetic: add an expected newline in proof_global.Hugo Herbelin
2018-03-06Rename some universe minimizing "normalize" functions to "minimize"Gaëtan Gilbert
2018-03-06Deprecate UState aliases in Evd.Gaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2018-02-15[toplevel] Make toplevel state into a record.Emilio Jesus Gallego Arias
2018-01-22Fix #6591: anomaly when using selectors outside of a proof.Cyprien Mangin
2018-01-11Force polymorphic definitions to have no internal constraints.Pierre-Marie Pédrot
2017-12-06Fix #6323: stronger restrict universe context vs abstract.Gaëtan Gilbert
2017-12-01Cleanup API for registering universe binders.Matthieu Sozeau
2017-11-29[proof] [api] Rename proof types in preparation for functionalization.Emilio Jesus Gallego Arias
2017-11-25Make restrict_universe_context stronger.Gaëtan Gilbert
2017-11-24In close_proof only check univ decls with the restricted context.Gaëtan Gilbert
2017-11-24Use Entries.constant_universes_entry more.Gaëtan Gilbert
2017-11-24When declaring constants/inductives use ContextSet if monomorphic.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 04:03:05 +0000