aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-03-09Merge PR #6775: Allow using cumulativity without forcing strict constraints.Maxime Dénès
2018-03-09Merge PR #6953: [default.nix] Pin nixpkgs version to include Sphinx dependenciesMaxime Dénès
2018-03-09Merge PR #6806: Adding missing unification constraint noticed by @skyskimmerMaxime Dénès
2018-03-09Merge PR #6769: Split closure cache and remove whd_bothMaxime Dénès
2018-03-09Merge PR #6923: Export optionsMaxime Dénès
2018-03-09[default.nix] Pin nixpkgs version to include Sphinx dependenciesVincent Laporte
2018-03-09[default.nix] minor cleaningVincent Laporte
2018-03-09Overlay for Elpi.Gaëtan Gilbert
2018-03-09Adjust EConstr.cmp_constructors for relaxed constructor cumulativityGaëtan Gilbert
2018-03-09Documentation for Cumulativity Weak Constraints.Gaëtan Gilbert
2018-03-09Delayed weak constraints for cumulative inductive types.Gaëtan Gilbert
2018-03-09Statically enforce that ULub is only between levels.Gaëtan Gilbert
2018-03-09Option for messing with inference of irrelevant constraintsGaëtan Gilbert
2018-03-09Cumulativity: improve treatment of irrelevant universes.Gaëtan Gilbert
2018-03-09Allow using cumulativity without forcing strict constraints.Gaëtan Gilbert
2018-03-09Merge PR #6480: Allow Prop as source for coercionsMaxime Dénès
2018-03-09Merge PR #6947: coqide: queries from the query window are routed there (fix #...Maxime Dénès
2018-03-09Adding a missing unification in typing.ml.Hugo Herbelin
2018-03-09Merge PR #6818: Sphinx doc infrastructureMaxime Dénès
2018-03-09Moving Gitlab CI documentation build to the main Coq build.Maxime Dénès
2018-03-09Integration of a sphinx-based documentation generator.Maxime Dénès
2018-03-09Configure now fails with -with-doc yes when a doc dependency is missing.Maxime Dénès
2018-03-09Merge PR #6895: [compat] Remove "Refolding Reduction" option.Maxime Dénès
2018-03-09Merge PR #6820: Tacticals assert_fails and assert_succeedsMaxime Dénès
2018-03-09Add an overlay for Equations and Ltac2.Pierre-Marie Pédrot
2018-03-09Documenting the Export modifier for options in CHANGES.Pierre-Marie Pédrot
2018-03-09Implement the Export Set/Unset feature.Pierre-Marie Pédrot
2018-03-09Export the various option localities in the API.Pierre-Marie Pédrot
2018-03-09doc and changes for coercion from prop/typecharguer
2018-03-09added test for coercion from typecharguer
2018-03-09allow Prop as source for coercionscharguer
2018-03-09Merge PR #6941: [toplevel] Respect COQ_COLORS environment variableMaxime Dénès
2018-03-09Merge PR #6945: Fix error with univ binders on monomorphic records.Maxime Dénès
2018-03-09Merge PR #6871: [build] Simpler byte/opt toplevel build.Maxime Dénès
2018-03-09Merge PR #6155: Get rid of ' notation for Zpos in QArithMaxime Dénès
2018-03-09Merge PR #6800: [checker] Printer cleanup.Maxime Dénès
2018-03-09Merge PR #6747: Relax conversion of constructors according to the pCuIC modelMaxime Dénès
2018-03-09Merge PR #6328: Fix #6313: lost goals in nested ltac in refineMaxime Dénès
2018-03-09Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec valuesMaxime Dénès
2018-03-09Merge PR #6496: Generate typed generic code from ltac macrosMaxime Dénès
2018-03-09Merge PR #6937: Add empty compat file for Coq 8.8Maxime Dénès
2018-03-09Merge PR #6851: Fix #6830: coqdep VDFILE uses too many arguments for fiat-cry...Maxime Dénès
2018-03-08More examples about shelve/given_up in tactic-in-terms.Hugo Herbelin
2018-03-08Cosmetic: add an expected newline in proof_global.Hugo Herbelin
2018-03-08A comment in Proofview.with_shelf.Hugo Herbelin
2018-03-08Add an invariant on future goals in Proof.run_tactic.Hugo Herbelin
2018-03-08Add an invariant on given up goals in class_tactics.Hugo Herbelin
2018-03-08Proof engine: support for nesting tactic-in-term within other tactics.Hugo Herbelin
2018-03-08Adding tclPUTGIVENUP/tclPUTSHELF in Proofview.Unsafe.Hugo Herbelin
2018-03-08Add function bind in option.ml.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 17:10:33 +0000