aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-11-29[proof] [api] Rename proof types in preparation for functionalization.Emilio Jesus Gallego Arias
In particular `Proof_global.t` will become a first class object for the upper parts of the system in a next commit.
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 ↵Maxime Dénès
of levels
2017-11-29Merge PR #6199: [vernac] Uniformize type of vernac interpretation.Maxime Dénès
2017-11-28Add PR backport script.Théo Zimmermann
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; ↵Maxime Dénès
updating Camlp4->Camlp5.
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
In particular, we put all the context in the atts structure, and generalize the type of the parameters of a vernac. I hope this helps people working on "attributes", my motivation is indeed having a more robust interpretation.
2017-11-27Merge PR #6237: coq_makefile tests: build in easily removed temporary ↵Maxime Dénès
subdirectory.
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
Was introduced in 0917ce7c to fix #4272, but it seems that we can fix it by just merging levels 10 and 11. This prevents the worry of fixing the associativity of level 11 to left in 0917ce7c.
2017-11-27Fixing associativity registered for level 10.Hugo Herbelin
Apparently a long-standing bug, coupled with a pattern/constr associativity inconsistency introduced while fixing another pattern/constr level inconsistency (bug #4272, 0917ce7c).
2017-11-26[api] Remove aliases of `Evar.t`Emilio Jesus Gallego Arias
There don't really bring anything, we also correct some minor nits with the printing function.
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
Note that this makes the following syntax valid: Axiom foo@{i} bar : Type@{i}. (ie putting a universe declaration on the first axiom in the list, the declaration then holds for the whole list).
2017-11-25Fix interpretation of global universes in univdecl constraints.Gaëtan Gilbert
Also nicer error when the constraints are impossible.
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
This fixes BZ#5717. Also add a test and fix a changed test.
2017-11-25Fix obligations handling of universes anticipating stronger restrictMatthieu Sozeau
2017-11-24[lib] Generalize Control.timeout type.Emilio Jesus Gallego Arias
We also remove some internal implementation details from the mli file, there due historical reasons.
2017-11-24Use Evarutil.has_undefined_evars for tactic has_evar.Gaëtan Gilbert
2017-11-24In close_proof only check univ decls with the restricted context.Gaëtan Gilbert
2017-11-24Use Entries.constant_universes_entry more.Gaëtan Gilbert
This reduces conversions between ContextSet/UContext and encodes whether we are polymorphic by which constructor we use rather than using some boolean.
2017-11-24When declaring constants/inductives use ContextSet if monomorphic.Gaëtan Gilbert
Also use constant_universes_entry instead of a bool flag to indicate polymorphism in ParameterEntry. There are a few places where we convert back to ContextSet because check_univ_decl returns a UContext, this could be improved.
2017-11-24restrict_universe_context: do not prune named universes.Gaëtan Gilbert
2017-11-24Fix defining non primitive projections with abstracted universes.Gaëtan Gilbert
I think this only affects printing (in the new test you would get [Var (0)] when printing runwrap) but is still ugly.
2017-11-24Register universe binders for record projections.Gaëtan Gilbert
2017-11-24Stop exposing UState.universe_context and its Evd wrapper.Gaëtan Gilbert
We can enforce properties through check_univ_decl, or get an arbitrary ordered context with UState.context / Evd.to_universe_context (the later being a new wrapper of the former).
2017-11-24Separate checking univ_decls and obtaining universe binder names.Gaëtan Gilbert
2017-11-24Use Maps and ids for universe bindersGaëtan Gilbert
Before sometimes there were lists and strings.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 04:03:25 +0000