aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proof_global.ml
Commit message (Expand)AuthorAge
* Simplify even further the declaration of primitive projections,Gravatar Matthieu Sozeau2014-08-30
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
* Uncountably many bullets (+,-,*,++,--,**,+++,...).Gravatar Hugo Herbelin2014-08-05
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
* Making the error message about bullets more precise.Gravatar Pierre Courtieu2014-07-31
* Fix handling of universes at the end of proofs, esp. for async proof processing.Gravatar Matthieu Sozeau2014-07-25
* When closing a proof, make sure that the types have their evar substituted.Gravatar Arnaud Spiwack2014-07-23
* Proof_global: an unused variable replaced by a wildcard.Gravatar Arnaud Spiwack2014-07-23
* Proof_global.start_dependent_proof: properly threads the sigma through the te...Gravatar Arnaud Spiwack2014-07-23
* Change the interface of proof_global to take an evar_map instead of a univers...Gravatar Arnaud Spiwack2014-07-23
* Feedback: LoadedFile + GoalsGravatar Enrico Tassi2014-07-11
* Force the final universe context of a proof only in poly || now case.Gravatar Matthieu Sozeau2014-06-24
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
* Safer entry point of primitive projections in the kernel, now it does recognizeGravatar Matthieu Sozeau2014-06-17
* - Fix in kernel conversion not folding the universe constraintsGravatar Matthieu Sozeau2014-05-26
* Another try at close_proof that should behave better w.r.t. exception handling.Gravatar Matthieu Sozeau2014-05-16
* - Fix treatment of global universe constraints which should be passed alongGravatar Matthieu Sozeau2014-05-06
* - Fix eq_constr_universes restricted to Sorts.equalGravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.Gravatar Matthieu Sozeau2014-05-06
* Fix issue #88: restrict_universe_context was wrongly forgetting about constra...Gravatar Matthieu Sozeau2014-05-06
* - Fix index-list to show computational relations for rewriting files.Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* Rework handling of universes on top of the STM, allowing for delayedGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* STM: fix valid_id coming from Qed errorsGravatar Enrico Tassi2014-02-10
* Proof_global: Simpler API for proof_terminatorGravatar Enrico Tassi2014-01-04
* Qed: feedback when type checking is doneGravatar Enrico Tassi2013-12-24
* Fix Admitted.Gravatar Arnaud Spiwack2013-12-04
* Proof_global: fix start_proof comment after the preceding commits.Gravatar Arnaud Spiwack2013-12-04
* Factoring(continued).Gravatar Arnaud Spiwack2013-12-04
* Refactoring: storing more information in the terminator closure.Gravatar Arnaud Spiwack2013-12-04
* The commands that initiate proofs are now in charge of what happens when proo...Gravatar Arnaud Spiwack2013-12-04
* Allow proofs to start with dependent goals.Gravatar Arnaud Spiwack2013-12-04
* Allowing proofs starting with a non-empty evarmap.Gravatar ppedrot2013-11-04
* Adds a tactic give_up.Gravatar aspiwack2013-11-02
* Adds a shelve tactic.Gravatar aspiwack2013-11-02
* New option Default Goal Selector.Gravatar aspiwack2013-11-02
* The tactic [admit] exits with the "unsafe" status.Gravatar aspiwack2013-11-02
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* Future: better doc + restore ~pure optimizationGravatar gareuselesinge2013-10-31
* proof modes: use ephemerons to represent them in proof stateGravatar gareuselesinge2013-10-18
* declaration_hooks use EphemeronGravatar gareuselesinge2013-10-18
* Future: ported to Ephemeron + exception enhancingGravatar gareuselesinge2013-10-18
* Moving side effects into evar_map. There was no reason to keep anotherGravatar ppedrot2013-10-05
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
* safe Conv_oracle state for type checkingGravatar gareuselesinge2013-08-30
* stm: (initial) support for -coq-slavesGravatar gareuselesinge2013-08-08