aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/declare.ml
Commit message (Expand)AuthorAge
* [general] Move files to directories matching linking order.Gravatar Emilio Jesus Gallego Arias2017-07-19
* Getting rid of AUContext abstraction breakers in Discharge.Gravatar Pierre-Marie Pédrot2017-07-13
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
* Fix bugsGravatar Amin Timany2017-06-16
* Change the place of inference after sect dischargeGravatar Amin Timany2017-06-16
* Using UInfoInd for universes in inductive typesGravatar Amin Timany2017-06-16
* Extend definition of inductives to include subtyping infoGravatar Amin Timany2017-06-16
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* Don't double up on periods in anomaliesGravatar Jason Gross2017-06-02
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * Allow flexible anonymous universes in instances and sorts.Gravatar Gaetan Gilbert2017-05-03
* | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/
* Moving Universes to the engine/ folder.Gravatar Pierre-Marie Pédrot2016-10-30
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\
| * Merge branch 'bug5036' into v8.6Gravatar Matthieu Sozeau2016-10-20
| |\
| | * Fix bug #5036 autorewrite, sections and universesGravatar Matthieu Sozeau2016-10-20
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\| |
| * | Merge remote-tracking branch 'github/pr/299' into v8.6Gravatar Maxime Dénès2016-09-30
| |\ \
| * | | Fix bug #5036 autorewrite, sections and universesGravatar Matthieu Sozeau2016-09-29
| | |/ | |/|
| | * Fix bug #4869, allow Prop, Set, and level names in constraints.Gravatar Matthieu Sozeau2016-09-29
| |/
* | Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
* | Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.Gravatar Maxime Dénès2016-09-20
* | Stylistic improvements in intf/decl_kinds.mli.Gravatar Maxime Dénès2016-09-20
* | Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* | Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Reuse the typing_flags datatype for inductives.Gravatar Pierre-Marie Pédrot2016-06-18
* Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
* Factorizing the uses of Declareops.safe_flags.Gravatar Pierre-Marie Pédrot2016-06-16
* Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\
| * Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
* | Univs: more robust Universe/Constraint decls #4816Gravatar Matthieu Sozeau2016-06-13
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-24 11:49:34 +0000