aboutsummaryrefslogtreecommitdiff
path: root/library/declare.ml
AgeCommit message (Expand)Author
2017-07-19[general] Move files to directories matching linking order.Emilio Jesus Gallego Arias
2017-07-13Getting rid of AUContext abstraction breakers in Discharge.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-16Fix bugs and add an option for cumulativityAmin Timany
2017-06-16Fix bugsAmin Timany
2017-06-16Change the place of inference after sect dischargeAmin Timany
2017-06-16Using UInfoInd for universes in inductive typesAmin Timany
2017-06-16Extend definition of inductives to include subtyping infoAmin Timany
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-06-02Don't double up on periods in anomaliesJason Gross
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-03Allow flexible anonymous universes in instances and sorts.Gaetan Gilbert
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2016-10-30Moving Universes to the engine/ folder.Pierre-Marie Pédrot
2016-10-24Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-20Merge branch 'bug5036' into v8.6Matthieu Sozeau
2016-10-20Fix bug #5036 autorewrite, sections and universesMatthieu Sozeau
2016-10-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-30Merge remote-tracking branch 'github/pr/299' into v8.6Maxime Dénès
2016-09-29Fix bug #5036 autorewrite, sections and universesMatthieu Sozeau
2016-09-29Fix bug #4869, allow Prop, Set, and level names in constraints.Matthieu Sozeau
2016-09-22Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Maxime Dénès
2016-09-20Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.Maxime Dénès
2016-09-20Stylistic improvements in intf/decl_kinds.mli.Maxime Dénès
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Unify location handling of error functions.Emilio Jesus Gallego Arias
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-18Reuse the typing_flags datatype for inductives.Pierre-Marie Pédrot
2016-06-18Moving the typing_flags to the environment.Pierre-Marie Pédrot
2016-06-16Factorizing the uses of Declareops.safe_flags.Pierre-Marie Pédrot
2016-06-16Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Pierre-Marie Pédrot
2016-06-14Assume totality: dedicated type rather than boolArnaud Spiwack
2016-06-13Univs: more robust Universe/Constraint decls #4816Matthieu Sozeau
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-01-29Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-23Fix bug #4503: mixing universe polymorphic and monomorphicMatthieu Sozeau
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-15Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Maxime Dénès
2016-01-14Changing "P is assumed" to "P is declared".Hugo Herbelin
2016-01-02Remove some useless type declarations.Guillaume Melquiond
2015-11-27Univs: entirely disallow instantiation of polymorphic constants withMatthieu Sozeau
2015-10-30Add a way to get the right fix_exn in external vernacular commandsMatthieu Sozeau
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-10-27Fix bugs 4389, 4390 and 4391 due to wrong handling of universe namesMatthieu Sozeau
2015-10-02Univs: Change intf of push_named_def to return the computed universeMatthieu Sozeau
2015-10-02Univs: refined handling of assumptionsMatthieu Sozeau
2015-10-02Univs: fix Universe vernacular, fix bug #4287.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:31:14 +0000