aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-03-15Adding a function to encode/decode string list into a single string.Hugo Herbelin
This encodes/decodes a list of string into a string in a way compatible with shell interpretation. On the contrary of Filename.quote which is for computer consumption, it introduces quotes for human consumption. The strategy is to split each string into substrings separated by simple quotes. Each substring is surrounted by single quotes if it contains a space. Otherwise, each backslash in the substring is doubled. The substrings are concatenated separated by backslash-protected single quote. The strings are then concatenated separated with spaces. The decoding is shell-like in the sense that it follows the rules of single quote, backslash and space.
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-13[funind] [cleanup] Remove unused function parametersEmilio Jesus Gallego Arias
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[cleanup] Remove unnecessary Map/Set module creationEmilio Jesus Gallego Arias
2020-03-13Fixing a non-protected try-with in class_tactics.ml.Hugo Herbelin
2020-03-13Double-checking at tclZERO entry that the exception is non critical.Hugo Herbelin
2020-03-13Deprecation of catchable_exception, to be replaced by noncritical in try-with.Hugo Herbelin
2020-03-13Removing catchable_exception test in tclOR/tclORELSE.Hugo Herbelin
Since tclOR/tclORELSE are not supposed to return critical exceptions, we don't need to replace catchable_exception by noncritical.
2020-03-13Replacing catchable_exception by noncritical in try-with blocks.Hugo Herbelin
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-12Documenting when exceptions are noncritical in the proof engineHugo Herbelin
2020-03-12Add changelogSimonBoulier
2020-03-12Add message at the end of search results about implicit argumentsSimonBoulier
2020-03-12Print implicit arguments in types of referencesSimonBoulier
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-18 04:26:20 +0000