aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-03-19Document all the existing attributes.Théo Zimmermann
And fix documentation following the removal of the Template Check flag in #11546.
2020-03-19Make Cumulative, NonCumulative and Private attributes.Théo Zimmermann
- Legacy attributes can now be specified in any order. - Legacy attribute Cumulative maps to universes(cumulative). - Legacy attribute NonCumulative maps to universes(noncumulative). - Legacy attribute Private maps to private(matching). We use "private(matching)" and not "private(match)" because we cannot use keywords within attributes.
2020-03-19Update fullGrammar and common.edit_mlg following #11839.Théo Zimmermann
2020-03-19Merge PR #11760: firstorder: default tactic is “auto with core”Théo Zimmermann
Reviewed-by: JasonGross Reviewed-by: Zimmi48
2020-03-19Merge PR #11860: [ci] [docker] Update to 4.09.1Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-19Merge PR #11795: Print implicit arguments in types of referencesHugo Herbelin
Ack-by: herbelin
2020-03-19Merge PR #11822: Grants #11692: clear dependent knows about let-inPierre-Marie Pédrot
Reviewed-by: JasonGross Reviewed-by: ppedrot
2020-03-19Merge PR #11735: Deprecating catchable_exceptionPierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: ppedrot
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
2020-03-19[stdlib] Remove a few `auto with *`Vincent Laporte
2020-03-18[ci] [docker] Update to 4.09.1Emilio Jesus Gallego Arias
That release includes non trivial changes related C compilers, in particular due to `-fno-common` support.
2020-03-18Merge PR #11607: Hide binder type in Ltac2Jason Gross
Reviewed-by: JasonGross Ack-by: SkySkimmer
2020-03-18Adding a round-trip test for binders.Pierre-Marie Pédrot
2020-03-18Actually use the binder type for Ltac2 that should be used in the kernel.Pierre-Marie Pédrot
That is, it contains the type of the binder so as not to rely on the relevance explicitly.
2020-03-18Hide the Ltac2 binder type.Pierre-Marie Pédrot
For robustness and it is better to leave it opaque. Users are not supposed to fiddle with it.
2020-03-18Merge PR #11559: Remove year in headers.Hugo Herbelin
Reviewed-by: jfehrle
2020-03-18Merge PR #11812: Add an Export locality to hintsThéo Zimmermann
Reviewed-by: Zimmi48 Ack-by: gares Ack-by: maximedenes
2020-03-18Merge PR #11839: Dead code in g_prim.mlgPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2020-03-18Adding overlays.Pierre-Marie Pédrot
2020-03-18Add documentation for the export hint.Pierre-Marie Pédrot
2020-03-18Export the user-facing attribute for hint locality.Pierre-Marie Pédrot
2020-03-18Also show unchanged headers.Théo Zimmermann
2020-03-18Remove dates in headers.Théo Zimmermann
Cf. discussion at #11559 and decision of Coq Call 2020-02-26.
2020-03-18Use a 3-valued flag for hint locality.Pierre-Marie Pédrot
We reuse the same type as for options, even though it is a bit ill-named. At least it allows to share code with it.
2020-03-18Hack a non-superglobal mode for hints.Pierre-Marie Pédrot
The current implementation was seemingly never thought for this kind of semantics. Everything is superglobal by construction, notably hint database creation and naming schemes. The new mode feels a bit hackish to me, at some point this should be fully reimplemented from scratch with a clear design in mind.
2020-03-18Change some ouput tests due to the printing of implicitsSimonBoulier
2020-03-18Merge PR #11746: Register commonly used names from the Reals library for ↵Théo Zimmermann
plugins (e.g. gappa) Reviewed-by: Zimmi48
2020-03-17Merge PR #11699: Comment difference between the 2 hashes on constrPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-17Merge PR #11825: [ci] [docker] Update components in Docker imageGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-17Merge PR #11811: Remove a positivity check when Positivity Checking is offGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-17Add test for PR11811 (disable a positivity check)SimonBoulier
2020-03-17Dead code in g_prim.mlgHugo Herbelin
2020-03-16[ci] Cleanup old overlays.Emilio Jesus Gallego Arias
2020-03-16[ci] [docker] Update components in Docker imageEmilio Jesus Gallego Arias
We bump ounit, odoc, and lablgtk3 ; so far this is routine maintenance.
2020-03-16Merge PR #11813: Fixed link to "match" syntax figures.Théo Zimmermann
Reviewed-by: Zimmi48
2020-03-16Merge PR #11831: [ci] Re-enable VST testingGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-15[ci] Re-enable VST testingEmilio Jesus Gallego Arias
VST has been fixed upstream, c.f. https://github.com/PrincetonUniversity/VST/issues/392
2020-03-14Fixes #11692 (clear dependent knows about let-in).Hugo Herbelin
2020-03-14Merge PR #10858: Implementing postponed constraints in TC resolutionGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego
2020-03-13Merge PR #11797: Dune build rules for doc_grammar and fullGrammar.Emilio Jesus Gallego Arias
Ack-by: ejgallego
2020-03-13Merge PR #11688: When parsing a negative integer, ensure that the minus sign ↵Emilio Jesus Gallego Arias
is contiguous to the number. Reviewed-by: ejgallego
2020-03-13Merge PR #11803: Update Azure MacOS version 10.13 -> 10.14Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-03-13Implementing postponed constraints in TC resolutionMatthieu Sozeau
A constraint can be stuck if it does not match any of the declared modes for its head (if there are any). In that case, the subgoal is postponed and the next ones are tried. We do a fixed point computation until there are no stuck subgoals or the set does not change (it is impossible to make it grow, as asserted in the code, because it is always a subset of the initial goals) This allows constraints on classes with modes to be treated as if they were in any order (yay for stability of solutions!). Also, ultimately it should free us to launch resolutions more agressively (avoiding issues like the ones seen in PR #10762). Add more examples of the semantics of TC resolution with apply in test-suite Properly catch ModeMatchFailure on calls to map_e* Add fixed bug 9058 to the test-suite Close #9058 Add documentation Fixes after Gaëtan's review. Main change is to not use exceptions for control-flow Update tactics/class_tactics.ml Clearer and more efficient mode mismatch dispatch Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> Remove exninfo argument
2020-03-13Update Azure MacOS version 10.13 -> 10.14Gaëtan Gilbert
10.13 is deprecated as an azure VM Close #11449
2020-03-13Merge PR #11805: Fix coqchk for primitive integers on 32bit arch with OCaml ↵Pierre-Marie Pédrot
>= 4.08 (#11624) Reviewed-by: ppedrot
2020-03-13Merge PR #11016: [proof] Remove duplication in the proof save path.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: herbelin
2020-03-13Merge PR #11804: [CI] test hierarchy builder as part of elpiGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-13Merge PR #11815: [ci] [doc] Point to actual docker instructions.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-13Merge PR #11003: [vernac] Remove deprecated function.Gaëtan Gilbert
Reviewed-by: SkySkimmer
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:33:23 +0000