aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-12-26Add rew dependent NotationsJason Gross
This way when users `Import EqNotations`, we get pretty-printing for equality `match` statements too.
2019-12-26Merge PR #11336: [ci] [gitlab] [bedrock] Build bedrock with 1 coreThéo Zimmermann
Reviewed-by: Zimmi48
2019-12-24Merge PR #11284: [meta] Add ltac2 information to META.Théo Zimmermann
Ack-by: Zimmi48
2019-12-24[meta] Add ltac2 information to META.Emilio Jesus Gallego Arias
Closes #11225 , we use a bit of a hack due to the way the Makefile installs this plugin.
2019-12-24[ci] [gitlab] [bedrock] Build bedrock with 1 coreEmilio Jesus Gallego Arias
Most workers these days have 1 core, and building bedrock with 2 cores in that setup seems to be too memory stressful.
2019-12-24Merge PR #11316: Windows: switch OCaml to 4.08.1Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-12-23Merge PR #11293: Rename files with Class in their name to make their role ↵Hugo Herbelin
clearer.
2019-12-23Merge PR #11274: [library] [cleanup] Remove code duplication.Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2019-12-23Windows: switch OCaml to 4.08.1Michael Soegtrop
- remove manual flexlink circular dependency handling - use standard configure process instead of hand made windows make files - enable parallel build - remove bootstrapping step (maybe should be there for release builds)
2019-12-23Merge PR #11324: [refman] Mention Ltac2 in intro.Pierre-Marie Pédrot
Reviewed-by: jfehrle
2019-12-23Merge PR #10760: Make rapply handle all numbers of underscoresPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2019-12-22Apply suggestions from code reviewThéo Zimmermann
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2019-12-22Rename files with Class in their name to make their role clearer.Pierre-Marie Pédrot
We restrict to those that are actually related to typeclasses, and perform the following renamings: Classops --> Coercionops Class --> ComCoercion
2019-12-22[refman] Mention Ltac2 in intro.Théo Zimmermann
2019-12-21Merge PR #11311: Fix handling of recursive notations with custom entriesHugo Herbelin
Reviewed-by: herbelin
2019-12-20Merge PR #11308: Fix complexity test-suite failure reporting on WinEnrico Tassi
Reviewed-by: gares
2019-12-20Add test cases for #9490 and #9532Maxime Dénès
2019-12-20Fix handling of recursive notations with custom entriesMaxime Dénès
Fixes #9532 Fixes #9490
2019-12-20Merge PR #11258: Coherence checking for coercionsEnrico Tassi
Reviewed-by: gares
2019-12-19Merge PR #11247: Use standard float and integer datatypes in Votour ↵Maxime Dénès
representation. Reviewed-by: maximedenes
2019-12-20Coherence checking for coercionsKazuhiko Sakaguchi
This change improves the relaxed ambiguous path condition of coercions (#9743) to check that any circular inheritance path of `C >-> C` is definitionally equal to the identity function of the class `C`. Moreover, for a new inheritance path `p : C >-> D` and existing (valid) one `q : C >-> D`, the new mechanism does not report the ambiguity of `p` and `q` if they have a common element, that is to say: `p = p1 @ [c] @ p2` and `q = q1 @ [c] @ q2` for some coercion `c` and inheritance paths `p1`, `p2`, `q1`, and `q2`. In that case, convertibility of `p1` and `q1`, also, `p2` and `q2` should be checked; thus, checking the ambiguity of `p` and `q` is redundant with them. If the new mechanism does not report any ambiguous path, the inheritance graph must be coherent [Barthe 1995, Sect. 3.2] [Saïbi 1997, Sect. 7]: 1. for any circular path `p : C >-> C`, `p` is definitionally equal to the identity function, and 2. for any two paths `p, q : C >-> D`, `p` and `q` are convertible. [Barthe 1995] Gilles Barthe, Implicit coercions in type systems, In: TYPES '95, LNCS, vol 1158, Springer, 1996, pp 1-15. [Saïbi 1997] Amokrane Saïbi, Typing algorithm in type theory with inheritance, In: POPL '97, ACM, 1997, pp 292-301.
2019-12-19Remove trailing \r in complexity measures for WindowsJason Gross
2019-12-19Better error reporting when res is not what is expectedJason Gross
c.f. https://dev.azure.com/coq/coq/_build/results?buildId=6485&view=logs&jobId=2d2b3007-3c5c-5840-9bb0-2b1ea49925f3&j=2d2b3007-3c5c-5840-9bb0-2b1ea49925f3&t=77aad734-2057-5694-9ae2-ee1f5f26eae8
2019-12-19Fix complexity test-suite failure reporting on WinJason Gross
Apparently `expr 1 \+ 1` is fine on Linux but not cygwin/Windows, where it fails with "syntax error". Similarly for `-` and `/`.
2019-12-19Revert "Fix #11303: skip complexity tests on windows even if bogomips found"Jason Gross
This reverts commit ec505a2fa67b0776b624be54417e06c6512f1734. A better fix is coming
2019-12-19Fix #11303: skip complexity tests on windows even if bogomips foundGaëtan Gilbert
Apparently the bogomips produced by cygwin are extra-bogo.
2019-12-18Merge PR #6090: Implement open recursion in the pretyperEnrico Tassi
Ack-by: SkySkimmer Reviewed-by: ejgallego Reviewed-by: gares
2019-12-18Merge PR #9786: Fix Equation's ci scriptPierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-12-18Merge PR #10616: Fix push_universe_context* interfaces to use a consistent ↵Pierre-Marie Pédrot
~strict flag Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: ppedrot
2019-12-18Merge PR #11027: Cleanup post #10647 (expose comind universe handling)Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-12-18Merge PR #11203: Make the string argument of `time` print correctlyPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2019-12-18Merge PR #11267: FIND_SKIP_DIRS (make): ignore all dot directoriesEnrico Tassi
Reviewed-by: gares
2019-12-18Merge PR #11123: Fix signal polling for OCaml 4.10Maxime Dénès
Ack-by: ejgallego
2019-12-18Merge PR #11263: [micromega] fix efficiency regressionMaxime Dénès
Reviewed-by: maximedenes
2019-12-17Type pretyping is part of the open recursionPierre-Marie Pédrot
2019-12-17Exporting the open-recursion style API.Pierre-Marie Pédrot
2019-12-17Implementing open recursion in the pretyper.Pierre-Marie Pédrot
For now, the API is unchanged and this commit only splits pretyping code for each glob_constr constructor into a record field.
2019-12-17failwith -> caml_failwithGuillaume Munch-Maccagnoni
2019-12-17Fatal error in VM if SIGINT was seen but no exception occured.Guillaume Munch-Maccagnoni
2019-12-17Fix signal polling for OCaml 4.10Guillaume Munch-Maccagnoni
Issue #10603
2019-12-17Merge PR #11299: [VM] fix volatile declarationEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-12-17[VM] fix volatile declarationGuillaume Munch-Maccagnoni
2019-12-17Merge PR #10762: Fix refine and eapply to mark shelved goals as ↵Maxime Dénès
non-resolvable, always Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-12-17[micromega] fix efficiency regressionFrédéric Besson
PR #9725 fixes completness bugs introduces some inefficiency. The current PR intends to fix the inefficiency while retaining completness. The fix removes a pre-processing step and instead relies on a more elaborate proof format introducing positivity constraints on the fly. Solve bootstrapping issues: RMicromega <-> Rbase <-> lia. Fixes #11063 and fixes #11242 and fixes #11270
2019-12-17Merge PR #11294: Advertise doc for master branch in README.Maxime Dénès
Reviewed-by: maximedenes
2019-12-16FIND_SKIP_DIRS (make): ignore all dot directoriesGaëtan Gilbert
Fix #11266
2019-12-16Merge PR #11291: Being explicit on existence of a remote link in stdlib to ↵Théo Zimmermann
avoid possible "breach of privacy" Reviewed-by: Zimmi48
2019-12-16Overlay for #11027Gaëtan Gilbert
2019-12-16Advertise doc for master branch in README.Théo Zimmermann
2019-12-16Don't pass (ignored) implicits to interp_mutual_inductive_constrGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:51:50 +0000