aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-03-18Merge PR #9777: [Nix] A few improvementsThéo Zimmermann
Reviewed-by: Zimmi48
2019-03-18[kernel] Fix compare_head_gen_leq_with to use [leq] on applicationsMatthieu Sozeau
This fixes an incompleteness of subtyping on cumulative inductives, where I@{i} A <= I@{j} A should imply i <= j, i = j or no relation depending on the variance of I's universe.
2019-03-18[ci] Guard broken jobs under an `UNRELIABLE = enabled` variable.Emilio Jesus Gallego Arias
This way, we can opt out of these development in our personal pipelines, so we don't risk being throttled by Gitlab.
2019-03-18Less conv_tab allocations when pushing relevances, esp skip_patternGaëtan Gilbert
2019-03-18[Manual] Parametrize -> ParametErizeLysxia
- Refine some `@term` into `@type`
2019-03-18Print more info before trying to push to coq-on-cachix.Théo Zimmermann
2019-03-18Update doc and changesKazuhiko Sakaguchi
2019-03-18[Manual] Move command Context after Let, and more polishingLysxia
- Refine some `@term` into `@type`
2019-03-18Don't lose the warning name when warning becomes error.Gaëtan Gilbert
2019-03-18Remove Term_typing.translate_mind indirectionGaëtan Gilbert
2019-03-18Use named_context_val for fast lookup in intern named referenceGaëtan Gilbert
2019-03-18Fix constr_matching on SPropGaëtan Gilbert
2019-03-18[ide] Address warning 50Vincent Laporte
2019-03-18fix documentation issues, and add entry to change logcharguer
2019-03-18[CoqIDE] dune rules for installing bindingsVincent Laporte
2019-03-18polishing documentation for coqide bindings, following @Zimmi48 commentscharguer
2019-03-18final polishing for coqide bindingscharguer
2019-03-18Latex to LaTexcharguer
2019-03-18documentation for unicode bindingscharguer
2019-03-18implementation installation of default unicode bindingscharguer
2019-03-18bindings files storagecharguer
2019-03-18binding generator for coqidecharguer
2019-03-18cosmetic changescharguer
2019-03-18support for coqide commande line argumentscharguer
2019-03-18working set of bindingscharguer
2019-03-18latex to unicode in coqidecharguer
2019-03-18Merge PR #9740: Make NotConvertibleVect exception internal to typeopsPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-03-18Merge PR #9794: Use local universe names when printing universe inconsistencyPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-03-18[nix] Update reference to nixpkgsVincent Laporte
2019-03-18[nix] Move nixpkgs.nix into the dev/ directoryVincent Laporte
2019-03-18[nix-ci] Use “master” versions of “coq-ext-lib” and “simple-io”Vincent Laporte
2019-03-18[nix-ci] Share the reference to nixpkgs with default.nixVincent Laporte
2019-03-18[nix] Store the reference to nixpkgs in a dedicated fileVincent Laporte
2019-03-17[Manual] Move doc on Let into Section mechanism, and more polishingLysxia
- Put "Section mechanism" example earlier
2019-03-17Use local universe names when printing universe inconsistencyGaëtan Gilbert
2019-03-17Merge PR #9787: iconv bedrock2 CI output to UTF-8Emilio Jesus Gallego Arias
Reviewed-by: SkySkimmer
2019-03-17iconv bedrock2 CI output to UTF-8Andres Erbsen
The timing diff script dies badly on non-utf8 input (https://github.com/coq/coq/issues/9767).
2019-03-17[Manual] Gather section-specific commands in Section documentation (fix #9704)Lysxia
2019-03-17[Manual] Improve chapter Type classes, and add mention of Context under VariableLysxia
- More consistent code indentation - Nest command variants properly - Make `Context` explanation a bit less terse, with more links - Typesetting bits, add some :cmd: links
2019-03-16Merge PR #9784: Add test-suite to Paramcoq CIEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-03-16Add test-suite to Paramcoq CIPierre Roux
2019-03-15Merge PR #9783: [ci] [gitlab] Replace YAML grafting by `extends: ` declaration.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-03-15[ci] [gitlab] Replace YAML grafting by `extends: ` declaration.Emilio Jesus Gallego Arias
This should in general be more robust as we don't need to remember to graft subsections.
2019-03-15Merge PR #9694: remove unused import of osEmilio Jesus Gallego Arias
Reviewed-by: JasonGross
2019-03-15Merge pull request coq/ltac2#93 from SkySkimmer/spropPierre-Marie Pédrot
Adapt to coq/coq#8817 (SProp)
2019-03-15Merge PR #8817: SProp: the definitionally proof irrelevant universePierre-Marie Pédrot
Ack-by: JasonGross Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: mattam82
2019-03-15Merge PR #9425: BinInt: 3 lemmas about testbit, mod _ 2^, onesVincent Laporte
Reviewed-by: vbgl
2019-03-15Remove clutter by moving historic unmaintained dev/doc files to an archive ↵Théo Zimmermann
subfolder.
2019-03-14Relax the ambiguous path condition of coercionKazuhiko Sakaguchi
The `Coercion` command did report many ambiguous paths when one declared multiple inheritances. This change makes the `Coercion` command to do not report them when 1. all the coercion in the potentially ambiguous paths respect the uniform inheritance condition and 2. functional compositions of the potentially ambiguous paths are convertible to each other. The first condition is not explicitly checked but is used to make the checking process of the second condition easy. The key idea of this change: Let us consider a sequence of coercion f_1 : C_1 >-> C_2, f_2 : C_2 >-> C_3, ..., f_n : C_n >-> C_(n+1) which respect the uniform inheritance condition and where the user-defined classes C_i have m_i parameters respectively (i <= n). The functional composition f_1 . ... . f_n can be expressed as follows: (fun x_1 ... x_(m_1) y => f_n _ ... _ (* m_n times repetition of holes *) (... (f_2 _ ... _ (* m_2 times repetition of holes *) (f_1 x_1 ... x_(m_1) y))...)), and the contents of all the holes can be determined (inferred) without leaving any existential variables in them thanks to the uniform inheritance condition. Misc: - A test case for this change: test-suite/output/relaxed_ambiguous_paths.v - Turn the ambiguous paths messages into warnings to do output test.
2019-03-14Merge PR #9771: Exposes Coq_micromega.dump_proof_term to allow a use ↵Vincent Laporte
independent from tactics Reviewed-by: vbgl
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-29 07:36:02 +0000