aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-18Rename Retypeops -> RelevanceopsGaëtan Gilbert
This module used to do retyping for the kernel in prototypes of SProp, but was switched to only relevance inference before the merge.
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-17Properly thread let-bindings in Funind principle construction.Pierre-Marie Pédrot
Fixes #11846: Funind fails to generate principles for terms with let bindings.
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-16Document coq_makefile behavior wrt -native-compiler yesPierre Roux
2020-03-16Fix coq-makefile/native1 testPierre Roux
This was accidentaly disabled by #6264 when no_native_compiler was renamed to native_compiler. Moreover, the (then unactivated test) was broken by commit 48ae6ce (part of #9088).
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-15Use quotes when "necessary" in the coqtop argument window.Hugo Herbelin
This is at least to be able to use spaces in file names (#11595). In practice it protects also \, ', ", and many other symbols.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 05:13:50 +0000