aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2019-03-14Fix various dummy Relevant in ssrGaëtan Gilbert
Unknown impact so no tests.
2019-03-14Overlays for SPropGaëtan Gilbert
2019-03-14Documentation for SPropGaëtan Gilbert
2019-03-14Add StrictProp.v with basic SProp related definitionsGaëtan Gilbert
2019-03-14Put [@inline] on CClosure.Mark functionsGaëtan Gilbert
2019-03-14Switch order eqappr/check relevance in conversion.Gaëtan Gilbert
This takes advantage of the mutability of the fconstr relevance mark.
2019-03-14mutable relevance marks in fconstrGaëtan Gilbert
2019-03-14Test for SkySkimmer/coq#13Gaëtan Gilbert
(NB: this needs relevance mark fixing)
2019-03-14Repair relevance marks in-kernel.Gaëtan Gilbert
Prevent errors when under annotating binders.
2019-03-14Enable proof irrelevance for SProp.Gaëtan Gilbert
2019-03-14Inductives in SProp, forbid primitive records with only sprop fieldsGaëtan Gilbert
For nonsquashed: Either - 0 constructors - primitive record
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
Kernel should be mostly correct, higher levels do random stuff at times.
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
Note currently it's impossible to define inductives in SProp because indtypes.ml and the pretyper aren't fully plugged.
2019-03-14Make Sorts.t privateGaëtan Gilbert
2019-03-14Fix Require in output test for reals syntaxGaëtan Gilbert
2019-03-14BinInt: 3 lemmas about testbit, mod _ 2^, onesAndres Erbsen
2019-03-14Merge PR #9691: [dune] [ide] Don't install the internal CoqIDE UI library.Théo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-21 17:59:50 +0000