aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-29Suppress warning message in stdlib.Guillaume Melquiond
2017-04-28Revert "Renaming allow_patvar flag of intern_gen into pattern_mode."Maxime Dénès
2017-04-28Revert "Using a more explicit algebraic type for evars of kind "MatchingVar"."Maxime Dénès
2017-04-28Using a more explicit algebraic type for evars of kind "MatchingVar".Hugo Herbelin
2017-04-28Renaming allow_patvar flag of intern_gen into pattern_mode.Hugo Herbelin
2017-04-28Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Maxime Dénès
2017-04-27Merge PR#414: Some more theory on powerRZ.Maxime Dénès
2017-04-27Merge PR#583: [toplevel] More work on error handling.Maxime Dénès
2017-04-27Merge PR#586: trivial cleanup commits which does not change Coq APIMaxime Dénès
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 PR#584: Give andb_prop a simpler proofMaxime Dénès
2017-04-27Merge PR#585: Small typo in commentMaxime Dénès
2017-04-27Merge branch 'v8.6'Pierre-Marie Pédrot
2017-04-27contracting the type of "Pfedit.solve_by_implicit_tactic"Matej Košík
2017-04-26Small typo in commentVadim Zaliva
2017-04-25Give andb_prop a simpler proofJason Gross
2017-04-25[toplevel] Remove unused parameter from `Vernac.process_expr`.Emilio Jesus Gallego Arias
2017-04-25[toplevel] Use exception information for error printing.Emilio Jesus Gallego Arias
2017-04-25Fix an optimization failure in tclPROGRESS.Pierre-Marie Pédrot
2017-04-25Fix an optimization failure in tclPROGRESS.Pierre-Marie Pédrot
2017-04-25Merge PR#567: Fix bug #5377: @? patterns broken.Maxime Dénès
2017-04-25Merge PR#578: Fix nsatz not recognizing real literals.Maxime Dénès
2017-04-24[toplevel] Don't check proofs in -quick mode.Emilio Jesus Gallego Arias
2017-04-24[toplevel] Don't mask critical exceptions in vernac interpretation.Emilio Jesus Gallego Arias
2017-04-24Adding a dedicated travis overlay for fiat-parsers.Pierre-Marie Pédrot
2017-04-24Removing various tactic compatibility layers in core tactics.Pierre-Marie Pédrot
2017-04-24Porting the firstorder plugin to the new tactic API.Pierre-Marie Pédrot
2017-04-24Removing compatibility layer in Leminv.Pierre-Marie Pédrot
2017-04-24Removing tactic compatibility layer in Command.Pierre-Marie Pédrot
2017-04-24Removing tactic compatibility layer in congruence.Pierre-Marie Pédrot
2017-04-24Removing tactic compatibility layer in Micromega.Pierre-Marie Pédrot
2017-04-24Fix the API of the new pf_constr_of_global.Pierre-Marie Pédrot
2017-04-24Removing trivial compatibility layer in refl_omega.Pierre-Marie Pédrot
2017-04-24Porting omega to the new tactic API.Pierre-Marie Pédrot
2017-04-24Removing trivial compatibility layer in omega.Pierre-Marie Pédrot
2017-04-24Porting generalize_dep to the new tactic engine.Pierre-Marie Pédrot
2017-04-24Removing the tclWEAK_PROGRESS tactical.Pierre-Marie Pédrot
2017-04-24Removing the tclNOTSAMEGOAL primitive from the API.Pierre-Marie Pédrot
2017-04-24Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.Maxime Dénès
2017-04-24Merge PR#574: Fix bug #5476: Ltac has an inconsistent view of hypotheses.Maxime Dénès
2017-04-24Merge PR#552: Miscelaneous commitsMaxime Dénès
2017-04-24Merge PR#577: Add bedrock targets src and facade to Travis CIMaxime Dénès
2017-04-24Merge PR#569: Documenting EConstr for developpers.Maxime Dénès
2017-04-24Merge PR#565: Remove VernacErrorMaxime Dénès
2017-04-24Merge PR#580: [ide] Fix #5482 "location for query commands" in IDE.Maxime Dénès
2017-04-24Merge PR#581: [toplevel] [emacs] Don't quote errors in emacs mode.Maxime Dénès
2017-04-24Merge PR#492: [travis] Pin camlp5 to the minimal version 6.14 for 4.02.3Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 15:30:10 +0000