aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-06-12zify: confusion between Pos2Z.inj_sub and Pos2Z.inj_sub_max (fix #5336)Pierre Letouzey
2017-06-12[lib] Remove obsolete state-management function add_frozen_stateEmilio Jesus Gallego Arias
2017-06-12Remove commented documentation for Show Tree.Théo Zimmermann
2017-06-12Fix ocamldebug for the APIGaëtan Gilbert
2017-06-12Remove Show Thesis command which was never implemented.Théo Zimmermann
2017-06-12Remove non-working Show Tree and Show Node commands.Théo Zimmermann
2017-06-12Remove more dead code (follow-up of previous commit).Théo Zimmermann
2017-06-12Remove Show Implicit Arguments command.Théo Zimmermann
2017-06-12Remove Show Goal "uid" command.Théo Zimmermann
2017-06-11Point ci-hott at a newer version of HoTTJason Gross
2017-06-11[proof] Deprecate redundant wrappers.Emilio Jesus Gallego Arias
2017-06-11Normalize deprecation notices of ./configureThéo Zimmermann
2017-06-10Remove remaining vo.itarget files (obsolete since PR #499)Pierre Letouzey
2017-06-10Fix Travis sectioningJason Gross
2017-06-10Remove (useless) aliases from the API.Matej Košík
2017-06-10[toplevel] Print error header on fatal batch error.Emilio Jesus Gallego Arias
2017-06-09Better sectioning on travis log printing in test-suiteJason Gross
2017-06-09A fix to #5414 (ident bound by ltac names now known for "match").Hugo Herbelin
2017-06-09Makefile.common: remove an obsolete comment after PR#499Pierre Letouzey
2017-06-08Mirror dpdgraph's travis test more accuratelyJason Gross
2017-06-08Remove coq-dpdgraph overlayJason Gross
2017-06-08Fix bug 5026 (the stdlib shouldn't define inconsistent notations).Théo Zimmermann
2017-06-08Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-08Remove overlay.Maxime Dénès
2017-06-08Merge PR#652: Put all plugins behind an "API".Maxime Dénès
2017-06-07Update .gitignoreJason Gross
2017-06-07[stm] More fixes for nested commands [bugzilla 5589]Emilio Jesus Gallego Arias
2017-06-07completing a sentence in a commentMatej Košík
2017-06-07[kernel] Improve proof using message, fixes bugzilla #3613Emilio Jesus Gallego Arias
2017-06-07add overlaysMatej Košík
2017-06-07Put "ssreflect" behind "API".Matej Košík
2017-06-07Put all plugins behind an "API".Matej Kosik
2017-06-07Merge PR#698: Trunk miscMaxime Dénès
2017-06-07Merge PR#717: [proof] Deprecate "proof mode" APIMaxime Dénès
2017-06-07Merge PR#669: Ssr mergeMaxime Dénès
2017-06-06Overlay.Maxime Dénès
2017-06-06Merge the ssr plugin.Maxime Dénès
2017-06-06Remove some overlays.Maxime Dénès
2017-06-06Merge PR#623: Remove the Sigma (monotonous state) API.Maxime Dénès
2017-06-06Overlays.Maxime Dénès
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-06-06Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a sh...Maxime Dénès
2017-06-06Merge PR#728: A few typos.Maxime Dénès
2017-06-06Merge PR#600: Some factorizations of ltac interpretation functions between ss...Maxime Dénès
2017-06-06Merge PR#638: Fix bug #5360: anomalies in typeclass resolution outputMaxime Dénès
2017-06-06Merge PR#716: Don't double up on periods in anomaliesMaxime Dénès
2017-06-06Merge PR#723: [travis] [fiat] Test also fiat-core.Maxime Dénès
2017-06-05Merge PR#724: Move README.ci to markdownMaxime Dénès
2017-06-05Merge PR#726: [stm] Solve bug 5577 "STM branch name is incorrect with Time"Maxime Dénès
2017-06-05Merge PR#722: [printing] Remove duplicated printing function.Maxime Dénès