aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-03-18Merge PR #9777: [Nix] A few improvementsThéo Zimmermann
2019-03-18[kernel] Fix compare_head_gen_leq_with to use [leq] on applicationsMatthieu Sozeau
2019-03-18[ci] Guard broken jobs under an `UNRELIABLE = enabled` variable.Emilio Jesus Gallego Arias
2019-03-18Less conv_tab allocations when pushing relevances, esp skip_patternGaëtan Gilbert
2019-03-18[Manual] Parametrize -> ParametErizeLysxia
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
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
2019-03-18Merge PR #9794: Use local universe names when printing universe inconsistencyPierre-Marie Pédrot
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
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
2019-03-17iconv bedrock2 CI output to UTF-8Andres Erbsen
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
2019-03-16Merge PR #9784: Add test-suite to Paramcoq CIEmilio Jesus Gallego Arias
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
2019-03-15[ci] [gitlab] Replace YAML grafting by `extends: ` declaration.Emilio Jesus Gallego Arias
2019-03-15Merge PR #9694: remove unused import of osEmilio Jesus Gallego Arias
2019-03-15Merge pull request coq/ltac2#93 from SkySkimmer/spropPierre-Marie Pédrot
2019-03-15Merge PR #8817: SProp: the definitionally proof irrelevant universePierre-Marie Pédrot
2019-03-15Merge PR #9425: BinInt: 3 lemmas about testbit, mod _ 2^, onesVincent Laporte
2019-03-15Remove clutter by moving historic unmaintained dev/doc files to an archive su...Théo Zimmermann
2019-03-14Relax the ambiguous path condition of coercionKazuhiko Sakaguchi
2019-03-14Merge PR #9771: Exposes Coq_micromega.dump_proof_term to allow a use independ...Vincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 08:55:36 +0000