aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2015-10-08STM: fix backtrace handlingEnrico Tassi
2015-10-08Goptions: new value type: optional stringEnrico Tassi
These options can be set to a string value, but also unset. Internal data is of type string option.
2015-10-07Remove the "exists" overrides from Program. (Fix bug #4360)Guillaume Melquiond
2015-10-07Fix bug #4069: f_equal regression.Matthieu Sozeau
2015-10-07Univs: fix FingerTree contrib.Matthieu Sozeau
Let merge_context_set be lenient when merging the context of side effects of an entry from solve_by_tac.
2015-10-07Test for record syntax parsing.Pierre-Marie Pédrot
2015-10-07Record fields accept an optional final semicolon separator.Pierre-Marie Pédrot
There is no such thing as the OPTSEP macro in Camlp4 so I had to expand it by hand.
2015-10-07Univs: add Strict Universe Declaration option (on by default)Matthieu Sozeau
This option disallows "declare at first use" semantics for universe variables (in @{}), forcing the declaration of _all_ universes appearing in a definition when introducing it with syntax Definition/Inductive foo@{i j k} .. The bound universes at the end of a definition/inductive must be exactly those ones, no extras allowed currently. Test-suite files using the old semantics just disable the option.
2015-10-06Fixing emacs output in debugging mode.Pierre Courtieu
Goal displaying during Debugging ltac is a notice message now. Other messages are debug messages. This does not change anything in coqide or coqtop, but allows proofgeneral to dispatch them in the right buffers (pg had to be fixed too).
2015-10-06Univs (pretyping): call vm_compute/native_compute with the currentMatthieu Sozeau
universe graph
2015-10-06Fix bug #4354: interpret hints in the right env and sigma.Matthieu Sozeau
2015-10-05Univs: fix bug #4288, Print Sorted generated backward < constraints.Matthieu Sozeau
2015-10-05Univs: fix printing bug #3797.Matthieu Sozeau
2015-10-05Update the .mailmap file.Guillaume Melquiond
The update process is as follows: run "git shortlog -s -e" and look for duplicate or missing contributors.
2015-10-05Univs: fix handling of evar_map in identity coercion construction.Matthieu Sozeau
2015-10-04Fix typo. (Fix bug #4355)Guillaume Melquiond
2015-10-02Mark the Coq.Compat files for documentation. (Fix bug #4353)Guillaume Melquiond
2015-10-02Updating versions history with data from Gérard.Hugo Herbelin
Adding Gérard's history file about V1-V5 versions.
2015-10-02Fixing error messages about Hint.Hugo Herbelin
2015-10-02Improving reference manual in that auto uses simple apply rather than apply.Hugo Herbelin
Still, there are small differences, e.g. on "use_metas_eagerly_in_conv_on_closed_terms", but also maybe in some amount of use of delta that Matthieu would know better than me if it matters or not in practice.
2015-10-02Update the history of versions with recent versions.Hugo Herbelin
2015-10-02Univs: Change intf of push_named_def to return the computed universeMatthieu Sozeau
context Let-bound definitions can be opaque but the whole universe context was not gathered to be discharged at section closing time.
2015-10-02Univs: refined handling of assumptionsMatthieu Sozeau
According to their polymorphic/non-polymorphic status, which imply that universe variables introduced with it are assumed to be >= or > Set respectively in the following definitions.
2015-10-02Univs: fix checker generating undeclared universes.Matthieu Sozeau
2015-10-02Univs: fix test-suite file for #4287, now properly rejected.Matthieu Sozeau
2015-10-02Univs: Remove test-suite file #3309Matthieu Sozeau
This relied on universes lower than Prop. A proper test for the sharing option should be found, -type-in-type is not enough either.
2015-10-02Univs: fix test-suite file (4301 is invalid, but a good regression test)Matthieu Sozeau
2015-10-02Fix after rebase...Matthieu Sozeau
2015-10-02Univs: forgot a substitution in mod_typing.Matthieu Sozeau
2015-10-02Univs: correct handling of with in modulesMatthieu Sozeau
For polymorphic and non-polymorphic parameters and definitions, fixes bugs #4298, #4294
2015-10-02Univs: the stdlib now needs 5 universesMatthieu Sozeau
Prop < Set < i for every global univ i
2015-10-02Univs: fix bug #4251, handling of template polymorphic constants.Matthieu Sozeau
2015-10-02Univs: update checkerMatthieu Sozeau
2015-10-02Univs: fixed 3685 by side-effect :)Matthieu Sozeau
2015-10-02Univs: minor fixes to test-suite filesMatthieu Sozeau
108 used an implicit lowering to Prop.
2015-10-02Univs: fix handling of evd's universes and side effects in build_by_tacticMatthieu Sozeau
2015-10-02Univs: fix semantics of Type in proof mode in universe-polymorphic modeMatthieu Sozeau
Allowing universes to be instantiated if the body of the proof requires it (the levels stay flexible). Not allowed for non-polymorphic cases, to be compatible with the stm's invariant that the type should not change.
2015-10-02Univs: fix minimization to allow lowering a universe to Set, not Prop.Matthieu Sozeau
2015-10-02Univs: fix inference of the lowest sort for records.Matthieu Sozeau
2015-10-02Univs: fix subtyping of polymorphic parameters.Matthieu Sozeau
2015-10-02Univs: fix evar_map handling in Hint processing.Matthieu Sozeau
2015-10-02Univs: fix test-suite file for HoTT/coq bug #120Matthieu Sozeau
2015-10-02Univs: test-suite file for bug #2016Matthieu Sozeau
2015-10-02Univs: test-suite file for #4301, subtyping of poly parametersMatthieu Sozeau
2015-10-02Univs: uncovered bug in strengthening of opaque polymorphic definitions.Matthieu Sozeau
2015-10-02Fix test-suite file for bug #3777Matthieu Sozeau
2015-10-02Fix test-suite file: failing earlier as expected.Matthieu Sozeau
2015-10-02Fix test-suite fileMatthieu 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 22:22:18 +0000