Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | * | | Remove unused [open] statements | Gaetan Gilbert | 2017-04-27 | |
| | * | | Micromega: do not use Filename.temp_dir_path, remove unused values | Gaetan Gilbert | 2017-04-27 | |
| | * | | Remove unused constructors | Gaetan Gilbert | 2017-04-27 | |
| | * | | Add [_] prefix to unused values which maybe should be kept | Gaetan Gilbert | 2017-04-27 | |
| | * | | Remove some unused values and types | Gaetan Gilbert | 2017-04-27 | |
| | * | | Rename Sos_lib.(||) -> parser_or to avoid (deprecated) Pervasives.or | Gaetan Gilbert | 2017-04-27 | |
| | * | | Disambiguate Polynomial.Hyp and Mfourier.Hyp -> Assum | Gaetan Gilbert | 2017-04-27 | |
| | * | | Use [method!] to override methods (warning 7) | Gaetan Gilbert | 2017-04-27 | |
| | * | | Fix omitted labels in function calls | Gaetan Gilbert | 2017-04-27 | |
| | * | | Remove unused [rec] keywords | Gaetan Gilbert | 2017-04-27 | |
| | * | | Locally disable some warnings. | Gaetan Gilbert | 2017-04-27 | |
* | | | | Merge PR#414: Some more theory on powerRZ. | Maxime Dénès | 2017-04-27 | |
|\ \ \ \ | |_|/ / |/| | | | ||||
* | | | | Merge PR#583: [toplevel] More work on error handling. | Maxime Dénès | 2017-04-27 | |
|\ \ \ \ | ||||
* \ \ \ \ | Merge PR#586: trivial cleanup commits which does not change Coq API | Maxime Dénès | 2017-04-27 | |
|\ \ \ \ \ | ||||
* \ \ \ \ \ | Merge PR#568: Remove tactic compatibility layer | Maxime Dénès | 2017-04-27 | |
|\ \ \ \ \ \ | ||||
| * | | | | | | Document the API changes. | Pierre-Marie Pédrot | 2017-04-27 | |
* | | | | | | | Merge PR#584: Give andb_prop a simpler proof | Maxime Dénès | 2017-04-27 | |
|\ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ | Merge PR#585: Small typo in comment | Maxime Dénès | 2017-04-27 | |
|\ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2017-04-27 | |
|\ \ \ \ \ \ \ \ \ | ||||
| | | | | * | | | | | contracting the type of "Pfedit.solve_by_implicit_tactic" | Matej Košík | 2017-04-27 | |
| |_|_|_|/ / / / / |/| | | | | | | | | ||||
| | * | | | | | | | Small typo in comment | Vadim Zaliva | 2017-04-26 | |
| |/ / / / / / / |/| | | | | | | | ||||
| | * | | | | | | Give andb_prop a simpler proof | Jason 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-25 | |
| * | | | | | | Fix an optimization failure in tclPROGRESS. | Pierre-Marie Pédrot | 2017-04-25 | |
* | | | | | | | Fix an optimization failure in tclPROGRESS. | Pierre-Marie Pédrot | 2017-04-25 | |
| * | | | | | | Merge PR#567: Fix bug #5377: @? patterns broken. | Maxime Dénès | 2017-04-25 | |
| |\ \ \ \ \ \ | ||||
* | \ \ \ \ \ \ | Merge PR#578: Fix nsatz not recognizing real literals. | Maxime Dénès | 2017-04-25 | |
|\ \ \ \ \ \ \ \ | ||||
| | | | | * | | | | [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-24 | |
| |_|_|_|/ / / / |/| | | | | | | | ||||
| | | | * | | | | Adding a dedicated travis overlay for fiat-parsers. | Pierre-Marie Pédrot | 2017-04-24 | |
| | | | * | | | | Removing various tactic compatibility layers in core tactics. | Pierre-Marie Pédrot | 2017-04-24 | |
| | | | * | | | | Porting the firstorder plugin to the new tactic API. | Pierre-Marie Pédrot | 2017-04-24 | |
| | | | * | | | | Removing compatibility layer in Leminv. | Pierre-Marie Pédrot | 2017-04-24 | |
| | | | * | | | | Removing tactic compatibility layer in Command. | Pierre-Marie Pédrot | 2017-04-24 | |
| | | | * | | | | Removing tactic compatibility layer in congruence. | Pierre-Marie Pédrot | 2017-04-24 | |
| | | | * | | | | Removing tactic compatibility layer in Micromega. | Pierre-Marie Pédrot | 2017-04-24 | |
| | | | * | | | | Fix the API of the new pf_constr_of_global. | Pierre-Marie Pédrot | 2017-04-24 | |
| | | | * | | | | Removing trivial compatibility layer in refl_omega. | Pierre-Marie Pédrot | 2017-04-24 | |
| | | | * | | | | Porting omega to the new tactic API. | Pierre-Marie Pédrot | 2017-04-24 | |
| | | | * | | | | Removing trivial compatibility layer in omega. | Pierre-Marie Pédrot | 2017-04-24 | |
| | | | * | | | | Porting generalize_dep to the new tactic engine. | Pierre-Marie Pédrot | 2017-04-24 | |
| | | | * | | | | Removing the tclWEAK_PROGRESS tactical. | Pierre-Marie Pédrot | 2017-04-24 | |
| | | | * | | | | Removing the tclNOTSAMEGOAL primitive from the API. | Pierre-Marie Pédrot | 2017-04-24 | |
| |_|_|/ / / / |/| | | | | | | ||||
* | | | | | | | Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag. | Maxime Dénès | 2017-04-24 | |
|\ \ \ \ \ \ \ | ||||
| | | | | | | * | refman: remember the old name of template polymorphism. | Gaetan Gilbert | 2017-04-24 | |
* | | | | | | | | Merge PR#574: Fix bug #5476: Ltac has an inconsistent view of hypotheses. | Maxime Dénès | 2017-04-24 | |
|\ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ | Merge PR#552: Miscelaneous commits | Maxime Dénès | 2017-04-24 | |
|\ \ \ \ \ \ \ \ \ | ||||
| | | | | * \ \ \ \ | Merge PR#577: Add bedrock targets src and facade to Travis CI | Maxime Dénès | 2017-04-24 | |
| | | | | |\ \ \ \ \ | ||||
* | | | | | \ \ \ \ \ | Merge PR#569: Documenting EConstr for developpers. | Maxime Dénès | 2017-04-24 | |
|\ \ \ \ \ \ \ \ \ \ \ |