aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2018-03-08Proof engine: using save_future_goal when relevant.Hugo Herbelin
2018-03-08Proof engine: adding a function to save future goals including principal one.Hugo Herbelin
2018-03-08Proof engine: consider the pair principal and future goals as an entity.Hugo Herbelin
2018-03-08Merge PR #6522: Fix core hint database issue #6521Maxime Dénès
2018-03-08Merge PR #6816: Adding mention of shelved/given-up status in Show ExistentialsMaxime Dénès
2018-03-08Merge PR #6928: gitlab: install num for all 4.06 jobsMaxime Dénès
2018-03-08Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish...Maxime Dénès
2018-03-08Merge PR #6893: Cleanup UState API usageMaxime Dénès
2018-03-08[compat] Remove "Refolding Reduction" option.Emilio Jesus Gallego Arias
2018-03-08Make most of TACTIC EXTEND macros runtime calls.Maxime Dénès
2018-03-08Merge PR #6918: romega: get rid of EConstr.UnsafeMaxime Dénès
2018-03-08coqide: queries from the query window are routed there (fix #5684)Enrico Tassi
2018-03-08Fix error with univ binders on monomorphic records.Gaëtan Gilbert
2018-03-08Merge PR #6817: [configure]: support for profilesMaxime Dénès
2018-03-08Fix SR breakage due to allowing fixpoints on non-rec valuesMatthieu Sozeau
2018-03-08Add test-suite file for cumulative constructorsMatthieu Sozeau
2018-03-08Leave cumul constructor universes as is during unifMatthieu Sozeau
2018-03-08Update checker to reflect rule on constructors of polymorphic inductive typesMatthieu Sozeau
2018-03-08Relax conversion of constructors according to the pCuIC modelMatthieu Sozeau
2018-03-08Merge PR #6743: Add notation {x & P} for sigTMaxime Dénès
2018-03-08Merge PR #6927: Add some missing flushes in configure.Maxime Dénès
2018-03-08Merge PR #6909: Deprecate Focus and UnfocusMaxime Dénès
2018-03-08Merge PR #6899: [compat] Remove "Standard Proposition Elimination"Maxime Dénès
2018-03-08Merge PR #6881: [windows] support -addon in build scriptMaxime Dénès
2018-03-08Merge PR #6582: Mangle auto-generated namesMaxime Dénès
2018-03-08Merge PR #6933: Standard headers for C and Python.Maxime Dénès
2018-03-08Merge PR #6934: Warn when using “Require” in a sectionMaxime Dénès
2018-03-08Merge PR #6924: Clean-up remove always false useeager argument.Maxime Dénès
2018-03-08Merge PR #6902: [compat] Remove "Discriminate Introduction"Maxime Dénès
2018-03-08Merge PR #6903: [compat] Remove "Shrink Abstract"Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-17 05:13:22 +0000