aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/command.ml
Commit message (Expand)AuthorAge
* - Do module substitution inside mind_record.Gravatar Matthieu Sozeau2014-07-25
* Properly add a Set lower bound on any polymorphic inductive in Type withGravatar Matthieu Sozeau2014-07-11
* Cleanup code related to the constraint solving, which sits now outside theGravatar Matthieu Sozeau2014-07-03
* Properly compute the transitive closure of the system of constraintsGravatar Matthieu Sozeau2014-07-03
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
* Fix computation of Type argument for Program's fix_proto.Gravatar Matthieu Sozeau2014-06-24
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* - Add "Show Universes" to print information about universes during a proof.Gravatar Matthieu Sozeau2014-06-16
* 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
* Fix handling of anonymous Type in template universe polymorphic inductivesGravatar Matthieu Sozeau2014-06-04
* - Fix treatment of global universe constraints which should be passed alongGravatar Matthieu Sozeau2014-05-06
* Proper calculation of constructor levels, forgetting the level of lets.Gravatar Matthieu Sozeau2014-05-06
* Retype application of fix_proto to get the right universes in ProgramGravatar Matthieu Sozeau2014-05-06
* Fix restrict_universe_context removing some universes that do appear in the t...Gravatar Matthieu Sozeau2014-05-06
* Fix declarations of monomorphic assumptionsGravatar Matthieu Sozeau2014-05-06
* Fix program Fixpoint not taking care of universes.Gravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Gravatar Yves Bertot2014-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
* Removing Autoinstance once and for all.Gravatar Pierre-Marie Pédrot2014-04-25
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Useless Evd.create_evar_defs.Gravatar Pierre-Marie Pédrot2013-12-30
* STM: capture type checking error (Closes: 3195)Gravatar Enrico Tassi2013-12-24
* Qed: feedback when type checking is doneGravatar Enrico Tassi2013-12-24
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
* Fixup bug 3145Gravatar pboutill2013-11-03
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* Future: better doc + restore ~pure optimizationGravatar gareuselesinge2013-10-31
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
* declaration_hooks use EphemeronGravatar gareuselesinge2013-10-18
* Future: ported to Ephemeron + exception enhancingGravatar gareuselesinge2013-10-18
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
* Removing almost all new_untyped_evar, and a bunch of Evd.add.Gravatar ppedrot2013-09-18
* get rid of closures in global/proof stateGravatar gareuselesinge2013-08-08
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Use the Hook module here and there.Gravatar ppedrot2013-05-12
* Use definition_entry to declare local definitionsGravatar gareuselesinge2013-05-09
* A uniformization step around understand_* and interp_* functions.Gravatar herbelin2013-05-09
* Uniformization: isevars -> evdref/sigma/evdGravatar herbelin2013-05-09
* Fixing r16487 on sharing evars between multiple parameters (missing List.rev).Gravatar herbelin2013-05-09
* Uniformizing the [if_warn] flag used for warning printing and putGravatar ppedrot2013-05-08
* Declaration of multiple hypotheses or parameters now share typingGravatar herbelin2013-05-08
* Share more information between constructors and arity of an inductiveGravatar herbelin2013-05-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 23:42:03 +0000