aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2015-10-21Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.Pierre-Marie Pédrot
2015-10-20Boxing the Goal.enter primitive into a record type.Pierre-Marie Pédrot
2015-10-19Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-18Constraining refine to monotonic functions.Pierre-Marie Pédrot
2015-10-18Miscellaneous typos, spacing, US spelling in comments or variable names.Hugo Herbelin
2015-10-17Clarifying and documenting the UState API.Pierre-Marie Pédrot
2015-10-17Lemmas accept the Local flag.Pierre-Marie Pédrot
2015-10-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-14Remove -vm flag of coqtop.Maxime Dénès
2015-10-14Fixing bug #4367: Wrong error message in unification.Pierre-Marie Pédrot
2015-10-13Fix some typos.Guillaume Melquiond
2015-10-12Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-12Fix Definition id := Eval <redexpr> in by passing the right universeMatthieu Sozeau
2015-10-10Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-09Code cleaning in VM (with Benjamin).Maxime Dénès
2015-10-09Fix Next Obligation to not raise an anomaly in case of mutualMatthieu Sozeau
2015-10-09Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-08Axioms now support the universe binding syntax.Pierre-Marie Pédrot
2015-10-08aux_file: export API to ease writing of a Proof Using annotator.Enrico Tassi
2015-10-08Proof using: let-in policy, optional auto-clear, forward closure*Enrico Tassi
2015-10-08Spawn: use each socket exclusively for writing or readingEnrico Tassi
2015-10-08Goptions: new value type: optional stringEnrico Tassi
2015-10-07Univs: fix FingerTree contrib.Matthieu Sozeau
2015-10-07Univs: add Strict Universe Declaration option (on by default)Matthieu Sozeau
2015-10-06Splitting kernel universe code in two modules.Pierre-Marie Pédrot
2015-10-06Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-05Univs: fix handling of evar_map in identity coercion construction.Matthieu Sozeau
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Fix after rebase...Matthieu Sozeau
2015-10-02Univs: fix inference of the lowest sort for records.Matthieu Sozeau
2015-10-02Univs: correcly compute the levels of records when they fall in Prop.Matthieu Sozeau
2015-10-02Univs/program: handle side effects in obligations.Matthieu Sozeau
2015-10-02Univs: fix Show Universes.Matthieu Sozeau
2015-10-02Univs: fix environment handling in scheme building.Matthieu Sozeau
2015-10-02Univs: fix after rebase (from_ctx/from_env)Matthieu Sozeau
2015-10-02Univs: fix many evar_map initializations and leaks.Matthieu Sozeau
2015-10-02Universes: enforce Set <= i for all Type occurrences.Matthieu Sozeau
2015-09-29Prevent States.intern_state and System.extern_intern from looking up files in...Guillaume Melquiond
2015-09-29Remove some uses of Loadpath.get_paths.Guillaume Melquiond
2015-09-28Make -load-vernac-object respect the loadpath.Guillaume Melquiond
2015-09-25Merge branch 'v8.5'Pierre-Marie Pédrot
2015-09-25The -require option now accepts a logical path instead of a physical one.Pierre-Marie Pédrot
2015-09-25Updating the documentation and the toolchain w.r.t. the change in -compile.Pierre-Marie Pédrot
2015-09-25The -compile option now accepts ".v" files and outputs a warning otherwise.Pierre-Marie Pédrot
2015-09-25Declare assumptions of well-founded definitions as unsafe.Arnaud Spiwack
2015-09-25Propagate `Guarded` flag from syntax to kernel.Arnaud Spiwack
2015-09-25Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming gua...Arnaud Spiwack
2015-09-23Hopefully better names to constructors of internal_flag, as discussedHugo Herbelin
2015-09-23Give a way to control if the decidable-equality schemes are built likeHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-23 06:58:41 +0000