aboutsummaryrefslogtreecommitdiff
path: root/library/global.ml
AgeCommit message (Expand)Author
2017-11-04[api] Deprecate all legacy uses of Name.Id in core.Emilio Jesus Gallego Arias
2017-07-26Removing template polymorphism for definitions.Pierre-Marie Pédrot
2017-07-26Remove a horrendous hack in Declare to retrieve exported side-effects.Pierre-Marie Pédrot
2017-07-13Remove the function Global.type_of_global_unsafe.Pierre-Marie Pédrot
2017-07-13Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.Pierre-Marie Pédrot
2017-07-13Safer API for Global.body_of_constant and variants.Pierre-Marie Pédrot
2017-07-13Safer API for Global.type_of_global_in_context.Pierre-Marie Pédrot
2017-07-11Moving the last bits of abtraction-breaking code out of the kernel.Pierre-Marie Pédrot
2017-07-11Safe API for accessing universe constraints of global references.Pierre-Marie Pédrot
2017-07-06Merge PR #853: Clean 'with Definition' implementation.Maxime Dénès
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-07-03Removing a few suspicious functions from the kernel.Pierre-Marie Pédrot
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-16Using UInfoInd for universes in inductive typesAmin Timany
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2016-10-30Moving Universes to the engine/ folder.Pierre-Marie Pédrot
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-18Moving the typing_flags to the environment.Pierre-Marie Pédrot
2016-06-18Adding a local type-in-type flag in kernel declarations.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-01-20Update copyright headers.Maxime Dénès
2015-11-20Univs: fix type_of_global_in_context not returning instantiated universe cont...Matthieu 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-09-25Propagate `Guarded` flag from syntax to kernel.Arnaud Spiwack
2015-07-10Option -type-in-type: added support in checker and making it contaminatingHugo Herbelin
2015-05-27Fix bug #4159Matthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-12-17Global: export the name of the summary entryEnrico Tassi
2014-10-13selective join/export of the safe_environmentEnrico Tassi
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-09-13Providing a -type-in-type option for collapsing the universe hierarchy.Hugo Herbelin
2014-08-30Simplify even further the declaration of primitive projections,Matthieu Sozeau
2014-08-03Move to a representation of universe polymorphic constants using indices for ...Matthieu Sozeau
2014-07-01Add toplevel commands to declare global universes and constraints.Matthieu Sozeau
2014-06-13Less ocaml warnings.Hugo Herbelin
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.Matthieu Sozeau
2014-05-06Fix interface for template polymorphism, cleaning up code in all typing algor...Matthieu Sozeau
2014-05-06Initial work on reintroducing old-style polymorphism for compatibility (the s...Matthieu Sozeau
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-03-14Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it hadPierre-Marie Pédrot
2014-03-11vi2vo: universes handling finally fixedEnrico Tassi
2014-01-04.vi files: .vo files without proofsEnrico Tassi
2013-10-31Conv_orable made functional and part of pre_envgareuselesinge
2013-10-18Future: ported to Ephemeron + exception enhancinggareuselesinge
2013-08-20Safe_typing code refactoringletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:34:27 +0000