aboutsummaryrefslogtreecommitdiff
path: root/proofs/proof_global.ml
AgeCommit message (Expand)Author
2014-07-25Fix handling of universes at the end of proofs, esp. for async proof processing.Matthieu Sozeau
2014-07-23When closing a proof, make sure that the types have their evar substituted.Arnaud Spiwack
2014-07-23Proof_global: an unused variable replaced by a wildcard.Arnaud Spiwack
2014-07-23Proof_global.start_dependent_proof: properly threads the sigma through the te...Arnaud Spiwack
2014-07-23Change the interface of proof_global to take an evar_map instead of a univers...Arnaud Spiwack
2014-07-11Feedback: LoadedFile + GoalsEnrico Tassi
2014-06-24Force the final universe context of a proof only in poly || now case.Matthieu Sozeau
2014-06-18Proofs now take and return an evar_universe_context, simplifying interfacesMatthieu Sozeau
2014-06-17Safer entry point of primitive projections in the kernel, now it does recognizeMatthieu Sozeau
2014-05-26- Fix in kernel conversion not folding the universe constraintsMatthieu Sozeau
2014-05-16Another try at close_proof that should behave better w.r.t. exception handling.Matthieu Sozeau
2014-05-06- Fix treatment of global universe constraints which should be passed alongMatthieu Sozeau
2014-05-06- Fix eq_constr_universes restricted to Sorts.equalMatthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.Matthieu Sozeau
2014-05-06Fix issue #88: restrict_universe_context was wrongly forgetting about constra...Matthieu Sozeau
2014-05-06- Fix index-list to show computational relations for rewriting files.Matthieu Sozeau
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06Rework handling of universes on top of the STM, allowing for delayedMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-02-10STM: fix valid_id coming from Qed errorsEnrico Tassi
2014-01-04Proof_global: Simpler API for proof_terminatorEnrico Tassi
2013-12-24Qed: feedback when type checking is doneEnrico Tassi
2013-12-04Fix Admitted.Arnaud Spiwack
2013-12-04Proof_global: fix start_proof comment after the preceding commits.Arnaud Spiwack
2013-12-04Factoring(continued).Arnaud Spiwack
2013-12-04Refactoring: storing more information in the terminator closure.Arnaud Spiwack
2013-12-04The commands that initiate proofs are now in charge of what happens when proo...Arnaud Spiwack
2013-12-04Allow proofs to start with dependent goals.Arnaud Spiwack
2013-11-04Allowing proofs starting with a non-empty evarmap.ppedrot
2013-11-02Adds a tactic give_up.aspiwack
2013-11-02Adds a shelve tactic.aspiwack
2013-11-02New option Default Goal Selector.aspiwack
2013-11-02The tactic [admit] exits with the "unsafe" status.aspiwack
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-10-31Future: better doc + restore ~pure optimizationgareuselesinge
2013-10-18proof modes: use ephemerons to represent them in proof stategareuselesinge
2013-10-18declaration_hooks use Ephemerongareuselesinge
2013-10-18Future: ported to Ephemeron + exception enhancinggareuselesinge
2013-10-05Moving side effects into evar_map. There was no reason to keep anotherppedrot
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-08-30safe Conv_oracle state for type checkinggareuselesinge
2013-08-08stm: (initial) support for -coq-slavesgareuselesinge
2013-08-08get rid of closures in global/proof stategareuselesinge
2013-08-08enhance marshallable option for freeze (minor TODO in safe_typing)gareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-12-14Modulification of identifierppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-22 02:55:49 +0000