aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2017-12-18Merge PR #6419: [vernac] Split `command.ml` into separate files.Maxime Dénès
2017-12-18Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.Maxime Dénès
2017-12-17[flags] Make program_mode a parameter for commands in vernac.Emilio Jesus Gallego Arias
2017-12-17[vernac] Split `command.ml` into separate files.Emilio Jesus Gallego Arias
2017-12-15Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml`Maxime Dénès
2017-12-15[econstr] Switch constrintern API to non-imperative style.Emilio Jesus Gallego Arias
2017-12-13Merge PR #6341: Fix anomaly in [Type foo] command, + print uctx like Check.Maxime Dénès
2017-12-13Merge PR #6251: [proof] Embed evar_map in RefinerError exception.Maxime Dénès
2017-12-13[econstr] Small cleanup in `vernac/lemmas`Emilio Jesus Gallego Arias
2017-12-13[econstr] Cleanup in `vernac/classes.ml`.Emilio Jesus Gallego Arias
2017-12-12Merge PR #6275: [summary] Allow typed projections from global state.Maxime Dénès
2017-12-11Merge PR #6270: [toplevel] Properly redirect stdout on `Redirect` vernac.Maxime Dénès
2017-12-11Fix anomaly in [Type foo] command, + print uctx like Check.Gaëtan Gilbert
2017-12-11[proof] Embed evar_map in RefinerError exception.Emilio Jesus Gallego Arias
2017-12-11Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.Maxime Dénès
2017-12-10[api] Remove kernel dependency on intf (Decl_kind)Emilio Jesus Gallego Arias
2017-12-09[summary] Adapt STM to the new Summary API.Emilio Jesus Gallego Arias
2017-12-09[summary] Allow typed projections from global state + rework of internals.Emilio Jesus Gallego Arias
2017-12-06Fix #6323: stronger restrict universe context vs abstract.Gaëtan Gilbert
2017-12-05Merge PR #890: Global universe declarationsMaxime Dénès
2017-12-04[vernac] Couple of tweaks missing from previous PRs.Emilio Jesus Gallego Arias
2017-12-01Cleanup API for registering universe binders.Matthieu Sozeau
2017-12-01Merge PR #6233: [proof] [api] Rename proof types in preparation for functiona...Maxime Dénès
2017-11-30Merge PR #1049: Remove obsolete localityMaxime Dénès
2017-11-30Merge PR #6244: [lib] [api] Introduce record for `object_prefix`Maxime Dénès
2017-11-30Merge PR #6193: Fix (partial) #4878: option to stop autodeclaring axiom as in...Maxime Dénès
2017-11-29Remove "obsolete_locality" and fix STM vernac classification.Maxime Dénès
2017-11-29[lib] [api] Introduce record for `object_prefix`Emilio Jesus Gallego Arias
2017-11-29[proof] [api] Rename proof types in preparation for functionalization.Emilio Jesus Gallego Arias
2017-11-29Merge PR #6199: [vernac] Uniformize type of vernac interpretation.Maxime Dénès
2017-11-28[toplevel] Properly redirect stdout on `Redirect` vernac.Emilio Jesus Gallego Arias
2017-11-28Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gaëtan Gilbert
2017-11-28Merge PR #1033: Universe binder improvementsMaxime Dénès
2017-11-28Merge PR #6248: [api] Remove aliases of `Evar.t`Maxime Dénès
2017-11-27[vernac] Adjust `interp` to pass polymorphic in the attributes.Emilio Jesus Gallego Arias
2017-11-27[vernac] Add polymorphic to the type of vernac interpration options.Emilio Jesus Gallego Arias
2017-11-27[vernac] Start to uniformize type of vernac interpretation.Emilio Jesus Gallego Arias
2017-11-27Merge PR #6241: [lib] Generalize Control.timeout type.Maxime Dénès
2017-11-27Merge PR #6041: Protecting the printing of filenames with spaceMaxime Dénès
2017-11-26[api] Remove aliases of `Evar.t`Emilio Jesus Gallego Arias
2017-11-25Restrict universe context when declaring constants in obligations.Gaëtan Gilbert
2017-11-25Fix #5347: unify declaration of axioms with and without bound univs.Gaëtan Gilbert
2017-11-25Universe binders survive sections, modules and compilation.Gaëtan Gilbert
2017-11-25Allow local universe renaming in Print.Gaëtan Gilbert
2017-11-25Fix obligations handling of universes anticipating stronger restrictMatthieu Sozeau
2017-11-24[lib] Generalize Control.timeout type.Emilio Jesus Gallego Arias
2017-11-24Use Entries.constant_universes_entry more.Gaëtan Gilbert
2017-11-24When declaring constants/inductives use ContextSet if monomorphic.Gaëtan Gilbert
2017-11-24Fix defining non primitive projections with abstracted universes.Gaëtan Gilbert
2017-11-24Register universe binders for record projections.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 08:49:47 +0000