aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Add some missing flushes in configure.Gravatar Maxime Dénès2018-03-06
* Merge PR #6917: Fix failing packaging job.Gravatar Maxime Dénès2018-03-06
|\
* \ Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ...Gravatar Maxime Dénès2018-03-06
|\ \
* \ \ Merge PR #6795: [ssreflect] Export parsing witnesses in mli file.Gravatar Maxime Dénès2018-03-06
|\ \ \
* \ \ \ Merge PR #6896: [compat] Remove NOOP deprecated options.Gravatar Maxime Dénès2018-03-06
|\ \ \ \
* \ \ \ \ Merge PR #6824: Remove deprecated options related to typeclasses.Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6900: [compat] Remove "Tactic Pattern Unification"Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6898: [compat] Remove "Intuition Iff Unfolding"Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6901: [compat] Remove "Injection L2R Pattern Order"Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ \ \ \
| | | | | | | | * Fix failing packaging job.Gravatar Théo Zimmermann2018-03-05
| |_|_|_|_|_|_|/ |/| | | | | | |
| | | | | | * | [ssreflect] Export parsing witnesses in mli file.Gravatar Emilio Jesus Gallego Arias2018-03-05
| |_|_|_|_|/ / |/| | | | | |
* | | | | | | Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monadGravatar Maxime Dénès2018-03-05
|\ \ \ \ \ \ \ \
| | | | | | | * | [compat] Remove NOOP and alias deprecated options.Gravatar Emilio Jesus Gallego Arias2018-03-04
| | | | | | * | | Remove deprecated options related to typeclasses.Gravatar Théo Zimmermann2018-03-04
| | | | | | |/ /
* | | | | | | | Merge PR #935: Handling evars in the VMGravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / |/| | | | | | |
| | * | | | | | ssr: ipats: V82.tactic ~nf_evars:false everywhereGravatar Enrico Tassi2018-03-04
| | * | | | | | Proofview: V82.tactic option to not normalize evarsGravatar Enrico Tassi2018-03-04
| | * | | | | | ssr: rewrite Ssripats and Ssrview in the tactic monadGravatar Enrico Tassi2018-03-04
| | * | | | | | tactics: export e_reduct_in_conclGravatar Enrico Tassi2018-03-04
| | * | | | | | reductionops: remove dead code "bind_assum"Gravatar Enrico Tassi2018-03-04
| | * | | | | | proofview: debug API to print a goalGravatar Enrico Tassi2018-03-04
* | | | | | | | Merge PR #6791: Removing compatibility support for versions older than 8.5.Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6736: [toplevel] Move beautify to its own pass.Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \ | |_|_|/ / / / / / |/| | | | | | | |
* | | | | | | | | Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6876: Unify Const_sorts and Const_type, and remove VsortGravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6846: Moving code for "simple induction"/"simple destruct" to coret...Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6885: [stm] Partial fix for bug #6884 [location missing from replay...Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6873: [toplevel] Update state when `Drop` exception is thrown [#6872]Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6882: Harden gitattributes against core.whitespace configuration.Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6879: Fix #6878: univ undefined for [with Definition] bad instance ...Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6676: [proofview] goals come with a stateGravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #915: Fix rewrite in * side conditionsGravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6735: [toplevel] [vernac] Remove Load hack and check / document sup...Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | * | | | | | Removing test for bug #2850.Gravatar Pierre-Marie Pédrot2018-03-03
| | | | | | | | | | | | | * | | | | | Adding a test file for evar handling in the VM.Gravatar Pierre-Marie Pédrot2018-03-03
| | | | | | | | | | | | | * | | | | | Handling evars in the VM.Gravatar Pierre-Marie Pédrot2018-03-03
| |_|_|_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | * | [compat] Remove "Tactic Pattern Unification"Gravatar Emilio Jesus Gallego Arias2018-03-03
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | * | [compat] Remove "Intuition Iff Unfolding"Gravatar Emilio Jesus Gallego Arias2018-03-03
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | * | [compat] Remove "Injection L2R Pattern Order"Gravatar Emilio Jesus Gallego Arias2018-03-03
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | |
| | | | | | | | | | | | * | | CHANGES entry for #6791.Gravatar Théo Zimmermann2018-03-02
| | | | | | | | | | | | * | | Remove 8.5 compatibility support.Gravatar Théo Zimmermann2018-03-02
| | | | | | | | | | | | * | | Remove VOld compatibility flag.Gravatar Théo Zimmermann2018-03-02
| | | | | | | | | | | | * | | Turn warning for deprecated notations on.Gravatar Théo Zimmermann2018-03-02
| | | | | | | | | | | | * | | Remove the deprecation for some 8.2-8.5 compatibility aliases.Gravatar Théo Zimmermann2018-03-02
| |_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | |
| | | | | | | | | * | | | | [VM] Unify Const_sorts and Const_type, and remove Vsort.Gravatar Maxime Dénès2018-03-02
| |_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | |
| | | | | | | * | | | | | [stm] Partial fix for bug #6884 [location missing from replay nodes]Gravatar Emilio Jesus Gallego Arias2018-03-02
| | | | | * | | | | | | | Harden gitattributes against core.whitespace configuration.Gravatar Gaëtan Gilbert2018-03-01
| |_|_|_|/ / / / / / / / |/| | | | | | | | | | |
| | | | * | | | | | | | Fix #6878: univ undefined for [with Definition] bad instance size.Gravatar Gaëtan Gilbert2018-03-01
| |_|_|/ / / / / / / / |/| | | | | | | | | |
| | * | | | | | | | | Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Gravatar Hugo Herbelin2018-03-01
| | | |_|/ / / / / / | | |/| | | | | | |