aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/obligations.ml
Commit message (Expand)AuthorAge
* Fix bug #3887: Better error message for "More than one program with unsolved ...Gravatar Pierre-Marie Pédrot2016-05-09
* Rename Ephemeron -> CEphemeron.Gravatar Maxime Dénès2016-03-04
* Implement support for universe binder lists in Instance and Program Fixpoint/...Gravatar Matthieu Sozeau2016-01-23
* Univs/Program: update the universe context with global universeGravatar Matthieu Sozeau2015-12-02
* Fix bug #4444: Next Obligation performed after a Section opening wasGravatar Matthieu Sozeau2015-12-02
* Univs: carry on universe substitution when defining obligations ofGravatar Matthieu Sozeau2015-11-24
* Allow program hooks to see the refined universe_context at the end of aGravatar Matthieu Sozeau2015-11-19
* Add a way to get the right fix_exn in external vernacular commandsGravatar Matthieu Sozeau2015-10-30
* Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* Fix Next Obligation to not raise an anomaly in case of mutualGravatar Matthieu Sozeau2015-10-09
* Univs: fix FingerTree contrib.Gravatar Matthieu Sozeau2015-10-07
* Univs/program: handle side effects in obligations.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix many evar_map initializations and leaks.Gravatar Matthieu Sozeau2015-10-02
* Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* Code cleaning in Obligations.Gravatar Pierre-Marie Pédrot2015-08-22
* obligations: wrap Ephemeron.get to make error more informativeGravatar Enrico Tassi2015-06-23
* Wrap the program_info type up in the ephemeron mechanismGravatar Alec Faithfull2015-06-23
* Program: Do not reduce obligation types preemptively, only atGravatar Matthieu Sozeau2015-04-13
* Add the possibility of defining opaque terms with program.Gravatar mlasson2015-01-21
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Tentatively more informative report of failure when inferringGravatar Hugo Herbelin2014-12-11
* Exporting the function handling side-effects only applied to terms.Gravatar Pierre-Marie Pédrot2014-11-20
* Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Gravatar Arnaud Spiwack2014-10-22
* Splitting out of auto.ml a file hints.ml dedicated to hints so as toGravatar Hugo Herbelin2014-10-07
* Merging some functions from evarutil.ml/evd.ml.Gravatar Hugo Herbelin2014-09-29
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* 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
* Fix program using an the unsubstituted type of the original obligationGravatar Matthieu Sozeau2014-08-14
* - Fix bug introduced in obligations which wouldn't consider all evars that areGravatar Matthieu Sozeau2014-07-16
* Better handling of the universe context in case of Admitted proof obligations.Gravatar Matthieu Sozeau2014-07-10
* When defining a monomorphic Program, do not allow arbitrary instantiationsGravatar Matthieu Sozeau2014-07-03
* 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
* Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofGravatar Pierre-Marie Pédrot2014-06-08
* Enforce a correct exception handling in declaration_hooksGravatar Enrico Tassi2014-06-08
* - Force every universe level to be >= Prop, so one cannot "go under" it anymore.Gravatar Matthieu Sozeau2014-06-04
* - Fix in kernel conversion not folding the universe constraintsGravatar Matthieu Sozeau2014-05-26
* - 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
* - Rename eq to equal in Univ, document new modules, set interfaces.Gravatar 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 many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Qed: feedback when type checking is doneGravatar Enrico Tassi2013-12-24
* Removing useless meta-related functions.Gravatar Pierre-Marie Pédrot2013-12-03
* Using hashes instead of strings in dynamic tags. In case of collision, anGravatar Pierre-Marie Pédrot2013-11-22
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 00:12:27 +0000