aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/declare.ml
Commit message (Expand)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\
| * Fix bug #4503: mixing universe polymorphic and monomorphicGravatar Matthieu Sozeau2016-01-23
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| * Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
* | Changing "P is assumed" to "P is declared".Gravatar Hugo Herbelin2016-01-14
* | Remove some useless type declarations.Gravatar Guillaume Melquiond2016-01-02
|/
* Univs: entirely disallow instantiation of polymorphic constants withGravatar Matthieu Sozeau2015-11-27
* 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 bugs 4389, 4390 and 4391 due to wrong handling of universe namesGravatar Matthieu Sozeau2015-10-27
* Univs: Change intf of push_named_def to return the computed universeGravatar Matthieu Sozeau2015-10-02
* Univs: refined handling of assumptionsGravatar Matthieu Sozeau2015-10-02
* Univs: fix Universe vernacular, fix bug #4287.Gravatar Matthieu Sozeau2015-10-02
* Hopefully better names to constructors of internal_flag, as discussedGravatar Hugo Herbelin2015-09-23
* Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorGravatar Enrico Tassi2015-02-14
* Fix bug when discharging universe constraints coming from variablesGravatar Matthieu Sozeau2015-01-13
* Update headers.Gravatar Maxime Dénès2015-01-12
* kernel/ind Change interface of declare_mind and declare_mutualGravatar Matthieu Sozeau2015-01-05
* Pass around information on the use of template polymorphism forGravatar Matthieu Sozeau2014-11-23
* STM: simplify how the term part of a side effect is retrievedGravatar Enrico Tassi2014-10-13
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Removing dead code relative to the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* 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
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* - Do module substitution inside mind_record.Gravatar Matthieu Sozeau2014-07-25
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
* Safer entry point of primitive projections in the kernel, now it does recognizeGravatar Matthieu Sozeau2014-06-17
* ind_tables: always declare side effects (Closes: HOTT#110)Gravatar Enrico Tassi2014-06-08
* Declare: fix Future managementGravatar Enrico Tassi2014-05-16
* - 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
* Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Gravatar Yves Bertot2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...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
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
* Qed: feedback when type checking is doneGravatar Enrico Tassi2013-12-24
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* ind_tables: properly handling side effectsGravatar gareuselesinge2013-08-30
* abstract+Defined: create opaque sub proofs (as pre-ParalITP)Gravatar gareuselesinge2013-08-19
* Removing useless casts between arrays and lists.Gravatar ppedrot2013-08-04
* Use the Hook module here and there.Gravatar ppedrot2013-05-12
* Use definition_entry to declare local definitionsGravatar gareuselesinge2013-05-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-24 11:47:18 +0000