aboutsummaryrefslogtreecommitdiff
path: root/library/declare.ml
AgeCommit message (Expand)Author
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
2015-09-25Propagate `Guarded` flag from syntax to kernel.Arnaud Spiwack
2015-09-23Hopefully better names to constructors of internal_flag, as discussedHugo Herbelin
2015-06-24Add a corresponding field in `mutual_inductive_entry` (part 1).Arnaud Spiwack
2015-02-14Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorEnrico Tassi
2015-01-13Fix bug when discharging universe constraints coming from variablesMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2015-01-05kernel/ind Change interface of declare_mind and declare_mutualMatthieu Sozeau
2014-11-23Pass around information on the use of template polymorphism forMatthieu Sozeau
2014-10-13STM: simplify how the term part of a side effect is retrievedEnrico Tassi
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-10-11Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 19:46:39 +0000