aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Expand)Author
2017-05-25Merge PR#637: Short cleaning of the interpretation path for constr_with_bindingsMaxime Dénès
2017-05-25Merge PR#481: [option] Remove support for non-synchronous options.Maxime Dénès
2017-05-25Merge PR#406: coq makefile2Maxime Dénès
2017-05-25[location] [travis] Add overlays for located_switchEmilio Jesus Gallego Arias
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-24[option] Remove support for non-synchronous options.Emilio Jesus Gallego Arias
2017-05-23overlay for UniMathEnrico Tassi
2017-05-23[vernac] Remove `Save thm id.` command.Emilio Jesus Gallego Arias
2017-05-22Clarifying the interpretation path for the "constr_with_binding" argument.Hugo Herbelin
2017-05-18Fix a typoJason Gross
2017-05-17Merge PR#633: An extension of EXTEND and notations to make standard parsing t...Maxime Dénès
2017-05-17Merge branch 'v8.6'Pierre-Marie Pédrot
2017-05-16Adding support for using grammar entries returning no value in EXTEND.Hugo Herbelin
2017-05-10Switch bedrock to mit-plv baseJason Gross
2017-05-08Fix warnings in top_printersGaetan Gilbert
2017-05-02Merge PR#582: Fix warningsMaxime Dénès
2017-05-01Add bmsherman/topology to the ciJason Gross
2017-05-01More consistent writing of de Bruijn.Théo Zimmermann
2017-05-01Fix for bug 5507. Mispelt de Bruijn.Théo Zimmermann
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-27Locally disable some warnings.Gaetan Gilbert
2017-04-27Merge PR#568: Remove tactic compatibility layerMaxime Dénès
2017-04-27Document the API changes.Pierre-Marie Pédrot
2017-04-27Merge branch 'v8.6'Pierre-Marie Pédrot
2017-04-25[located] [doc] Improve docs for `CAst.ast`.Emilio Jesus Gallego Arias
2017-04-25[travis] mathcomp and fiat overlay for #402Emilio Jesus Gallego Arias
2017-04-25[location] Document changes.Emilio Jesus Gallego Arias
2017-04-25[location] Remove `Loc.internal_ghost`Emilio Jesus Gallego Arias
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-24[location] Switch glob_constr to Loc.locatedEmilio Jesus Gallego Arias
2017-04-24Adding a dedicated travis overlay for fiat-parsers.Pierre-Marie Pédrot
2017-04-20Add bedrock targets src and facadeJason Gross
2017-04-19Documenting EConstr for developpers.Pierre-Marie Pédrot
2017-04-15Merge branch 'v8.6' into trunkMaxime Dénès
2017-04-14Fix EOL characters in xml protocol documentation.Maxime Dénès
2017-04-14Merge PR#563: add XML protocol doc for 8.6Maxime Dénès
2017-04-14[travis] Use the lite target for fiat-crypto.Maxime Dénès
2017-04-13update XML protocol doc to 8.6Paul Steckler
2017-04-13add XML protocol doc for 8.5Paul Steckler
2017-04-12Merge PR#441: Port Toplevel to the Stm APIMaxime Dénès
2017-04-12[stm] Improve error messages on add/parse.Emilio Jesus Gallego Arias
2017-04-12[stm] Port the toplevel to the STM.Emilio Jesus Gallego Arias
2017-04-12[stm] Move main parsing entry point to the STM.Emilio Jesus Gallego Arias
2017-04-12Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...Maxime Dénès
2017-04-11Merge PR#379: Introducing evar-insensitive constrsMaxime Dénès
2017-04-07Merge PR#461: [camlpX] Remove camlp4 compat layer.Maxime Dénès
2017-04-07Fixes for Drop. to work (decl_mode removal and toplevel -> vernac)Matthieu Sozeau
2017-04-07Merge branch 'master' into econstrPierre-Marie Pédrot
2017-04-07[travis] Overlay for PR#461: Camlp4 removal.Emilio Jesus Gallego Arias
2017-04-06Adding a documentation for the new proof engine.Pierre-Marie Pédrot