aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-03-07gitlab: install num for all jobsGaëtan Gilbert
2018-03-06Merge PR #6917: Fix failing packaging job.Maxime Dénès
2018-03-06Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ...Maxime Dénès
2018-03-06Merge PR #6795: [ssreflect] Export parsing witnesses in mli file.Maxime Dénès
2018-03-06Merge PR #6896: [compat] Remove NOOP deprecated options.Maxime Dénès
2018-03-06Merge PR #6824: Remove deprecated options related to typeclasses.Maxime Dénès
2018-03-06Merge PR #6900: [compat] Remove "Tactic Pattern Unification"Maxime Dénès
2018-03-06Merge PR #6898: [compat] Remove "Intuition Iff Unfolding"Maxime Dénès
2018-03-06Merge PR #6901: [compat] Remove "Injection L2R Pattern Order"Maxime Dénès
2018-03-05Fix failing packaging job.Théo Zimmermann
2018-03-05[ssreflect] Export parsing witnesses in mli file.Emilio Jesus Gallego Arias
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-05Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monadMaxime Dénès
2018-03-04[compat] Remove NOOP and alias deprecated options.Emilio Jesus Gallego Arias
2018-03-04Remove deprecated options related to typeclasses.Théo Zimmermann
2018-03-04Merge PR #935: Handling evars in the VMMaxime Dénès
2018-03-04ssr: ipats: V82.tactic ~nf_evars:false everywhereEnrico Tassi
2018-03-04Proofview: V82.tactic option to not normalize evarsEnrico Tassi
2018-03-04ssr: rewrite Ssripats and Ssrview in the tactic monadEnrico Tassi
2018-03-04tactics: export e_reduct_in_conclEnrico Tassi
2018-03-04reductionops: remove dead code "bind_assum"Enrico Tassi
2018-03-04proofview: debug API to print a goalEnrico Tassi
2018-03-04Merge PR #6791: Removing compatibility support for versions older than 8.5.Maxime Dénès
2018-03-04Merge PR #6736: [toplevel] Move beautify to its own pass.Maxime Dénès
2018-03-04Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Maxime Dénès
2018-03-04Merge PR #6876: Unify Const_sorts and Const_type, and remove VsortMaxime Dénès
2018-03-04Merge PR #6846: Moving code for "simple induction"/"simple destruct" to coret...Maxime Dénès
2018-03-04Merge PR #6885: [stm] Partial fix for bug #6884 [location missing from replay...Maxime Dénès
2018-03-04Merge PR #6873: [toplevel] Update state when `Drop` exception is thrown [#6872]Maxime Dénès
2018-03-04Merge PR #6882: Harden gitattributes against core.whitespace configuration.Maxime Dénès
2018-03-04Merge PR #6879: Fix #6878: univ undefined for [with Definition] bad instance ...Maxime Dénès
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-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 "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-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-01Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Hugo Herbelin