aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-03-04Merge PR #6676: [proofview] goals come with a stateMaxime Dénès
2018-03-04Merge PR #915: Fix rewrite in * side conditionsMaxime Dénès
2018-03-04Merge PR #6735: [toplevel] [vernac] Remove Load hack and check / document sup...Maxime Dénès
2018-03-04Remove whd_both from the kernel.Pierre-Marie Pédrot
2018-03-04Pass the constant cache as a separate argument in kernel reduction.Pierre-Marie Pédrot
2018-03-04Remove all uses of Focus in standard library.Théo Zimmermann
2018-03-04Fix typos.Théo Zimmermann
2018-03-03Removing test for bug #2850.Pierre-Marie Pédrot
2018-03-03Adding a test file for evar handling in the VM.Pierre-Marie Pédrot
2018-03-03Handling evars in the VM.Pierre-Marie Pédrot
2018-03-03[compat] Remove "Tactic Pattern Unification"Emilio Jesus Gallego Arias
2018-03-03[compat] Remove "Standard Proposition Elimination"Emilio Jesus Gallego Arias
2018-03-03[compat] Remove "Intuition Iff Unfolding"Emilio Jesus Gallego Arias
2018-03-03[compat] Remove "Injection L2R Pattern Order"Emilio Jesus Gallego Arias
2018-03-02CHANGES entry for #6791.Théo Zimmermann
2018-03-02Remove 8.5 compatibility support.Théo Zimmermann
2018-03-02Remove VOld compatibility flag.Théo Zimmermann
2018-03-02Turn warning for deprecated notations on.Théo Zimmermann
2018-03-02Remove the deprecation for some 8.2-8.5 compatibility aliases.Théo Zimmermann
2018-03-02[VM] Unify Const_sorts and Const_type, and remove Vsort.Maxime Dénès
2018-03-02installer: win: put addons in a separate packageEnrico Tassi
2018-03-02build: win: detect 404 as HTML filesEnrico Tassi
2018-03-02build: win: addon bignumsEnrico Tassi
2018-03-02build: win: support for addonsEnrico Tassi
2018-03-02[stm] Partial fix for bug #6884 [location missing from replay nodes]Emilio Jesus Gallego Arias
2018-03-01Harden gitattributes against core.whitespace configuration.Gaëtan Gilbert
2018-03-01Fix #6878: univ undefined for [with Definition] bad instance size.Gaëtan Gilbert
2018-03-01Add source (project file / command line) to project fields.Gaëtan Gilbert
2018-03-01Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Hugo Herbelin
2018-03-01Moving code for "simple induction"/"simple destruct" to coretactics.ml4.Hugo Herbelin
2018-03-01Merge PR #6856: travis: elpi needs findlib >= 1.5Maxime Dénès
2018-03-01Merge PR #6864: Remove empty, wrongly located, doc file.Maxime Dénès
2018-03-01Merge PR #6861: Typo in the documentation of the `pattern` tacticMaxime Dénès
2018-03-01Merge PR #6850: Fix #6751 trust_file_cache logic was invertedMaxime Dénès
2018-03-01[coq] Adapt to coq/coq#6511Emilio Jesus Gallego Arias
2018-03-01[api] Remove some deprecation warnings.Emilio Jesus Gallego Arias
2018-02-28[toplevel] Update state when `Drop` exception is thrown [#6872]Emilio Jesus Gallego Arias
2018-02-28Uniform spacing layout in Tactics.v.Hugo Herbelin
2018-02-28Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross).Hugo Herbelin
2018-02-28[toplevel] Move beautify to its own pass.Emilio Jesus Gallego Arias
2018-02-28[test-suite] Add a basic test-case for `Load`.Emilio Jesus Gallego Arias
2018-02-28[toplevel] [vernac] Remove Load hack and check supported scenarios.Emilio Jesus Gallego Arias
2018-02-28[econstr] Continue consolidation of EConstr API under `interp`.Emilio Jesus Gallego Arias
2018-02-28travis: elpi needs findlib >= 1.5Enrico Tassi
2018-02-28tavis: make the . in pkg.version part of $VERSIONEnrico Tassi
2018-02-28appveyor: build non-experimental tasks firstEnrico Tassi
2018-02-28Merge PR #6847: Fix make source-docMaxime Dénès
2018-02-28Fix #6830: coqdep VDFILE uses too many arguments for fiat-crypto/OSXGaëtan Gilbert
2018-02-28Merge PR #6854: comment "resolvability" bit in Evd.evar_mapMaxime Dénès
2018-02-28Merge PR #6852: [stdlib] move “Require” out of sectionsMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-23 06:51:17 +0000