aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/command.ml
Commit message (Expand)AuthorAge
* Pass around information on the use of template polymorphism forGravatar Matthieu Sozeau2014-11-23
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Change reduction_of_red_expr to return an e_reduction_function returningGravatar Matthieu Sozeau2014-10-24
* Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Gravatar Arnaud Spiwack2014-10-22
* Fixing #3193 (honoring implicit arguments in local definitions).Gravatar Hugo Herbelin2014-10-03
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Fix categorization of recursive inductives.Gravatar Matthieu Sozeau2014-09-10
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
* Fixing bug #3492.Gravatar Pierre-Marie Pédrot2014-09-07
* Types declared as Variants really do not accept recursive definitions.Gravatar Arnaud Spiwack2014-09-04
* Simplify even further the declaration of primitive projections,Gravatar Matthieu Sozeau2014-08-30
* Fixing commit 50237af2.Gravatar Pierre-Marie Pédrot2014-08-29
* Fixing bug #3528.Gravatar Pierre-Marie Pédrot2014-08-28
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
* - 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-01 17:45:31 +0000