aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* [default.nix] minor cleaningGravatar Vincent Laporte2018-03-09
* Merge PR #6480: Allow Prop as source for coercionsGravatar Maxime Dénès2018-03-09
|\
* \ Merge PR #6947: coqide: queries from the query window are routed there (fix #...Gravatar Maxime Dénès2018-03-09
|\ \
* \ \ Merge PR #6818: Sphinx doc infrastructureGravatar Maxime Dénès2018-03-09
|\ \ \
| * | | Moving Gitlab CI documentation build to the main Coq build.Gravatar Maxime Dénès2018-03-09
| * | | Integration of a sphinx-based documentation generator.Gravatar Maxime Dénès2018-03-09
| * | | Configure now fails with -with-doc yes when a doc dependency is missing.Gravatar Maxime Dénès2018-03-09
* | | | Merge PR #6895: [compat] Remove "Refolding Reduction" option.Gravatar Maxime Dénès2018-03-09
|\ \ \ \
* \ \ \ \ Merge PR #6820: Tacticals assert_fails and assert_succeedsGravatar Maxime Dénès2018-03-09
|\ \ \ \ \
| | | | | * doc and changes for coercion from prop/typeGravatar charguer2018-03-09
| | | | | * added test for coercion from typeGravatar charguer2018-03-09
| | | | | * allow Prop as source for coercionsGravatar charguer2018-03-09
| |_|_|_|/ |/| | | |
* | | | | Merge PR #6941: [toplevel] Respect COQ_COLORS environment variableGravatar Maxime Dénès2018-03-09
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6945: Fix error with univ binders on monomorphic records.Gravatar Maxime Dénès2018-03-09
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6871: [build] Simpler byte/opt toplevel build.Gravatar Maxime Dénès2018-03-09
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6155: Get rid of ' notation for Zpos in QArithGravatar Maxime Dénès2018-03-09
|\ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / |/| | | | | | |
* | | | | | | | Merge PR #6800: [checker] Printer cleanup.Gravatar Maxime Dénès2018-03-09
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6747: Relax conversion of constructors according to the pCuIC modelGravatar Maxime Dénès2018-03-09
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6328: Fix #6313: lost goals in nested ltac in refineGravatar Maxime Dénès2018-03-09
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec valuesGravatar Maxime Dénès2018-03-09
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6496: Generate typed generic code from ltac macrosGravatar Maxime Dénès2018-03-09
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6937: Add empty compat file for Coq 8.8Gravatar Maxime Dénès2018-03-09
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6851: Fix #6830: coqdep VDFILE uses too many arguments for fiat-cry...Gravatar Maxime Dénès2018-03-09
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | * | | | | | | | | | More examples about shelve/given_up in tactic-in-terms.Gravatar Hugo Herbelin2018-03-08
| | | | | * | | | | | | | | | Cosmetic: add an expected newline in proof_global.Gravatar Hugo Herbelin2018-03-08
| | | | | * | | | | | | | | | A comment in Proofview.with_shelf.Gravatar Hugo Herbelin2018-03-08
| | | | | * | | | | | | | | | Add an invariant on future goals in Proof.run_tactic.Gravatar Hugo Herbelin2018-03-08
| | | | | * | | | | | | | | | Add an invariant on given up goals in class_tactics.Gravatar Hugo Herbelin2018-03-08
| | | | | * | | | | | | | | | Proof engine: support for nesting tactic-in-term within other tactics.Gravatar Hugo Herbelin2018-03-08
| | | | | * | | | | | | | | | Adding tclPUTGIVENUP/tclPUTSHELF in Proofview.Unsafe.Gravatar Hugo Herbelin2018-03-08
| | | | | * | | | | | | | | | Add function bind in option.ml.Gravatar Hugo Herbelin2018-03-08
| | | | | * | | | | | | | | | Proof engine: using save_future_goal when relevant.Gravatar Hugo Herbelin2018-03-08
| | | | | * | | | | | | | | | Proof engine: adding a function to save future goals including principal one.Gravatar Hugo Herbelin2018-03-08
| | | | | * | | | | | | | | | Proof engine: consider the pair principal and future goals as an entity.Gravatar Hugo Herbelin2018-03-08
| |_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | |
* | | | | | | | | | | | | | Merge PR #6522: Fix core hint database issue #6521Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6816: Adding mention of shelved/given-up status in Show ExistentialsGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6928: gitlab: install num for all 4.06 jobsGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish...Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6893: Cleanup UState API usageGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | * | [compat] Remove "Refolding Reduction" option.Gravatar Emilio Jesus Gallego Arias2018-03-08
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | |
| | | | | | | | * | | | | | | | | | Make most of TACTIC EXTEND macros runtime calls.Gravatar Maxime Dénès2018-03-08
| |_|_|_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | Merge PR #6918: romega: get rid of EConstr.UnsafeGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | * coqide: queries from the query window are routed there (fix #5684)Gravatar Enrico Tassi2018-03-08
| | | | | | | | | | | | | | * | | | Fix error with univ binders on monomorphic records.Gravatar Gaëtan Gilbert2018-03-08
* | | | | | | | | | | | | | | | | | Merge PR #6817: [configure]: support for profilesGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | * | | | | | | | | Fix SR breakage due to allowing fixpoints on non-rec valuesGravatar Matthieu Sozeau2018-03-08
| | | | | | | | | | | * | | | | | | | Add test-suite file for cumulative constructorsGravatar Matthieu Sozeau2018-03-08
| | | | | | | | | | | * | | | | | | | Leave cumul constructor universes as is during unifGravatar Matthieu Sozeau2018-03-08
| | | | | | | | | | | * | | | | | | | Update checker to reflect rule on constructors of polymorphic inductive typesGravatar Matthieu Sozeau2018-03-08
| | | | | | | | | | | * | | | | | | | Relax conversion of constructors according to the pCuIC modelGravatar Matthieu Sozeau2018-03-08
| | | | | | | | | | | | |_|_|/ / / / | | | | | | | | | | | |/| | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-28 22:11:33 +0000