aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2017-12-30Returning instance instead of substitution in universe context abstraction.Pierre-Marie Pédrot
2017-12-29[vernac] adds the “program” flag to the “atts” recordVincent Laporte
2017-12-29Merge PR #6492: Remove query-in-IDE warning.Maxime Dénès
2017-12-29Merge PR #6405: Remove the local polymorphic flag hack.Maxime Dénès
2017-12-29Merge PR #6433: [flags] Move global time flag into an attribute.Maxime Dénès
2017-12-27Remove query-in-IDE warning.Maxime Dénès
2017-12-27Remove the local polymorphic flag hack.Maxime Dénès
2017-12-27Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.Maxime Dénès
2017-12-27Merge PR #6443: [vernac] Cleanup of do_definition.Maxime Dénès
2017-12-27Merge PR #6289: Remove unused boolean from cl_context field of Typeclasses.ty...Maxime Dénès
2017-12-23[api] Also deprecate constructors of Decl_kinds.Emilio Jesus Gallego Arias
2017-12-23[flags] Move global time flag into an attribute.Emilio Jesus Gallego Arias
2017-12-21Merge code paths in interp_definition and cleanup a bit.Gaëtan Gilbert
2017-12-20Separate vernac controls and regular commands.Maxime Dénès
2017-12-18[vernac] Cleanup of do_definition.Emilio Jesus Gallego Arias
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-30Remove unused boolean from cl_context field of Typeclasses.typeclassGaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 20:42:37 +0000