aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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 #6274: Attempt to fix inversion disregarding singleton types (fixes ...Maxime Dénès
2017-11-30Merge PR #6269: [ci] [vst] Shorten compilation time to avoid Travis timeouts.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-29Merge PR #6271: Add PR backport script.Maxime Dénès
2017-11-29Merge PR #6253: Fixing inconsistent associativity of level 10 in the table of...Maxime Dénès
2017-11-29Merge PR #6199: [vernac] Uniformize type of vernac interpretation.Maxime Dénès
2017-11-28In injection/inversion, consider all template-polymorphic types as injectable.Hugo Herbelin
2017-11-28Adding a variant get_truncation_family_of of get_sort_family_of.Hugo Herbelin
2017-11-28Moving non-recursive function sort_family_of out of the retype block of recur...Hugo Herbelin
2017-11-28Add PR backport script.Théo Zimmermann
2017-11-28[ci] [vst] Shorten compilation time to avoid Travis timeouts.Emilio Jesus Gallego Arias
2017-11-28Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gaëtan Gilbert
2017-11-28Merge PR #6259: Add PR merge script.Maxime Dénès
2017-11-28Add PR merge script.Maxime Dénès
2017-11-28Merge PR #1033: Universe binder improvementsMaxime Dénès
2017-11-28Merge PR #6235: Fixing failing mkdir in test-suite for coq-makefile.Maxime Dénès
2017-11-28Merge PR #6248: [api] Remove aliases of `Evar.t`Maxime Dénès
2017-11-28Merge PR #6246: Ref. Man.: Updating the current official writing of OCaml; up...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 #6237: coq_makefile tests: build in easily removed temporary subdire...Maxime Dénès
2017-11-27Merge PR #6242: Use Evarutil.has_undefined_evars for tactic has_evar.Maxime Dénès
2017-11-27Merge PR #6236: Fix coq-makefile ocamldoc call when configured with -annotate.Maxime Dénès
2017-11-27Merge PR #6207: [stm] Allow delayed constant in interactive mode.Maxime Dénès
2017-11-27Merge PR #6238: Fix deprecated syntax warning from vernacextend.mlp.Maxime Dénès
2017-11-27Merge PR #6241: [lib] Generalize Control.timeout type.Maxime Dénès
2017-11-27Merge PR #6228: Make byte on gitlab.Maxime Dénès
2017-11-27Merge PR #6226: Enhance votourMaxime Dénès
2017-11-27Merge PR #6149: Update TimeFileMaker.py to correctly sort timing diffsMaxime Dénès
2017-11-27Merge PR #6041: Protecting the printing of filenames with spaceMaxime Dénès
2017-11-27Merge PR #6227: Linter: do not lint untracked files.Maxime Dénès
2017-11-27A cosmetic standardization: adding a space in g_constr.ml4.Hugo Herbelin
2017-11-27Releasing level "11" of "pattern".Hugo Herbelin
2017-11-27Fixing associativity registered for level 10.Hugo Herbelin
2017-11-26[api] Remove aliases of `Evar.t`Emilio Jesus Gallego Arias
2017-11-25Overlay for stronger restrict_universe_context.Gaëtan Gilbert
2017-11-25Restrict universe context when declaring constants in obligations.Gaëtan Gilbert
2017-11-25Updating the current official writing of OCaml, updating Camlp4->Camlp5.Hugo Herbelin
2017-11-25Fix #5347: unify declaration of axioms with and without bound univs.Gaëtan Gilbert
2017-11-25Fix interpretation of global universes in univdecl constraints.Gaëtan Gilbert
2017-11-25Forbid repeated names in universe binders.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-25Make restrict_universe_context stronger.Gaëtan Gilbert
2017-11-25Fix obligations handling of universes anticipating stronger restrictMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-06 10:28:45 +0000