aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-03-18Merge PR #11839: Dead code in g_prim.mlgPierre-Marie Pédrot
Reviewed-by: ppedrot
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-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
2020-03-13[lemmas] Consolidate some declaration data on Info.tEmilio Jesus Gallego Arias
Now that `MutualEntry` provides a more uniform interface we can reuse `Info.t` In the medium term we shall consolidate `Proof` / `Proof_global` and `Lemmas` so admitted / finish are uniform too.
2020-03-12[declare] Remove trivial wrapperEmilio Jesus Gallego Arias
In preparation for the introduction of an opaque mutual definition type at the `Declare` level we remove the not very useful wrapper `declare_fix`. Now we should be ready to profit from `DeclareDef` and its handling of common stuff such as `restrict_universe_context` and `check_univ_decl` etc...
2020-03-12[lemmas] Handle mutual lemmas more uniformly.Emilio Jesus Gallego Arias
We split the paths for mutual / non-mutual constants, and we enforce some further invariants, in particular we avoid messing around with the body of saved constants, and using the indirect accessor. This should be almost semantically equivalent to the previous code, including some questionable choices present there. In further cleanups we will move this code to Declare, which should hopefully help clarify some of the semantics.
2020-03-12[save proof] Declare universe_binders unconditionally for mutual assumptions.Emilio Jesus Gallego Arias
As suggested by Gaëtan in review, we move declaration of universe binders to the common code in `DeclareDef`; this changes the semantics for the assumption case when Recthms is not empty.
2020-03-12[proof] Remove duplication in the proof save path.Emilio Jesus Gallego Arias
We move towards more unification in the proof save path of interactive and non-interactive proofs.
2020-03-12[vernac] Minor cleanup of opens in `Vernacentries`Emilio Jesus Gallego Arias
2020-03-12Merge PR #11796: Remove parallel building of Sphinx documentation.Emilio Jesus Gallego Arias
2020-03-12[ci] [doc] Point to actual docker instructions.Emilio Jesus Gallego Arias
2020-03-12Update doc/sphinx/addendum/extended-pattern-matching.rstlarsr
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
2020-03-12Fixed link to "match" syntax. larsr
and removed the now incorrect "section 8.2.3" reference, as it is the same as the "refine" link.
2020-03-12Merge PR #11798: Tests make bytecodeEnrico Tassi
Ack-by: SkySkimmer Reviewed-by: gares
2020-03-12Merge PR #11781: Minor improvements to the unreleased changelog.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2020-03-12Merge PR #11780: Minor improvements to the unreleased changelog.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2020-03-12Merge PR #11810: [dune] Fix ocamlopt_flags for release profileThéo Zimmermann
Reviewed-by: Zimmi48
2020-03-12Dune build rules for doc_grammar and fullGrammar.Théo Zimmermann
2020-03-12Add changelog entrySimonBoulier
2020-03-12Remove a positivity check when Check Positivity is offSimonBoulier
2020-03-12[dune] Fix ocamlopt_flags for release profileEmilio Jesus Gallego Arias
Closes #11758 It turns out that we were overwriting the default `ocamlopt_flags`, thus creating a problem in the release build.
2020-03-11Merge PR #11754: [micromega] Add numerical compatibility layer.Frédéric Besson
Ack-by: SkySkimmer Reviewed-by: fajb
2020-03-11Merge PR #11800: [ci] [gitlab] Move VST to `allow_failure`Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-11Update dev/ci/ci-basic-overlay.shEnrico Tassi
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-03-11Fix coqchk for primitive integers on 32bit arch with OCaml >= 4.08 (#11624)Pierre Roux
2020-03-11[CI] test hierarchy builder as part of elpiEnrico Tassi
2020-03-11Comment difference between the 2 hashes on constrGaëtan Gilbert
2020-03-11Merge PR #11769: Fix #9930: "change" replaces 0-param projections by constantsPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-11Merge PR #11786: Fix #11730: Mangle Names vs InfixPierre-Marie Pédrot
Reviewed-by: herbelin Reviewed-by: ppedrot
2020-03-11Merge PR #11790: [lib] [ccalgo] Remove unused code / cleanupPierre-Marie Pédrot
Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 16:26:29 +0000