aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Add .dir-locals.el to pluginsGravatar Jason Gross2017-05-18
* Merge PR#633: An extension of EXTEND and notations to make standard parsing t...Gravatar Maxime Dénès2017-05-17
|\
* \ Merge PR#607: Make congruence reuse discriminate instead of rolling its own.Gravatar Maxime Dénès2017-05-17
|\ \
| | * Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND.Gravatar Hugo Herbelin2017-05-16
| | * Adding support for using grammar entries returning no value in EXTEND.Gravatar Hugo Herbelin2017-05-16
* | | Typo in a comment of plugin Quote.Gravatar Hugo Herbelin2017-05-13
| |/ |/|
* | Merge PR#201: Transparent abstractGravatar Maxime Dénès2017-05-11
|\ \
* \ \ Merge PR#612: Set Ltac Batch DebugGravatar Maxime Dénès2017-05-09
|\ \ \
* | | | Prevent user-defined ring morphisms from ever being evaluated.Gravatar Guillaume Melquiond2017-05-09
| * | | Adding an option "Set Ltac Batch Debug" to additionally run Ltac debug in bat...Gravatar Hugo Herbelin2017-05-04
|/ / /
| | * Make congruence reuse discriminate instead of rolling its own.Gravatar Gaetan Gilbert2017-05-03
| |/ |/|
* | Post-rebase warnings (unused opens and 2 unused values)Gravatar Gaetan Gilbert2017-04-27
* | Fix 4.04 warningsGravatar Gaetan Gilbert2017-04-27
* | Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* | Micromega: do not use Filename.temp_dir_path, remove unused valuesGravatar Gaetan Gilbert2017-04-27
* | Remove unused constructorsGravatar Gaetan Gilbert2017-04-27
* | Add [_] prefix to unused values which maybe should be keptGravatar Gaetan Gilbert2017-04-27
* | Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
* | Rename Sos_lib.(||) -> parser_or to avoid (deprecated) Pervasives.orGravatar Gaetan Gilbert2017-04-27
* | Disambiguate Polynomial.Hyp and Mfourier.Hyp -> AssumGravatar Gaetan Gilbert2017-04-27
* | Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
* | Remove unused [rec] keywordsGravatar Gaetan Gilbert2017-04-27
* | Merge PR#568: Remove tactic compatibility layerGravatar Maxime Dénès2017-04-27
|\ \
| | * Add transparent_abstract tacticGravatar Jason Gross2017-04-25
| |/ |/|
* | Merge PR#578: Fix nsatz not recognizing real literals.Gravatar Maxime Dénès2017-04-25
|\ \
| | * Removing various tactic compatibility layers in core tactics.Gravatar Pierre-Marie Pédrot2017-04-24
| | * Porting the firstorder plugin to the new tactic API.Gravatar Pierre-Marie Pédrot2017-04-24
| | * Removing tactic compatibility layer in congruence.Gravatar Pierre-Marie Pédrot2017-04-24
| | * Removing tactic compatibility layer in Micromega.Gravatar Pierre-Marie Pédrot2017-04-24
| | * Fix the API of the new pf_constr_of_global.Gravatar Pierre-Marie Pédrot2017-04-24
| | * Removing trivial compatibility layer in refl_omega.Gravatar Pierre-Marie Pédrot2017-04-24
| | * Porting omega to the new tactic API.Gravatar Pierre-Marie Pédrot2017-04-24
| | * Removing trivial compatibility layer in omega.Gravatar Pierre-Marie Pédrot2017-04-24
| |/ |/|
* | Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Maxime Dénès2017-04-24
|\ \
* \ \ Merge PR#565: Remove VernacErrorGravatar Maxime Dénès2017-04-24
|\ \ \
* \ \ \ Merge branch v8.6 into trunkGravatar Hugo Herbelin2017-04-22
|\ \ \ \
| | * | | Remove VernacErrorGravatar Gaetan Gilbert2017-04-21
| |/ / / |/| | |
| | * | [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Emilio Jesus Gallego Arias2017-04-21
| |/ / |/| |
| | * Fix nsatz not recognizing real literals.Gravatar Guillaume Melquiond2017-04-20
| |/ |/|
* | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
|\ \
* | | Silence a few OCaml warnings.Gravatar Guillaume Melquiond2017-04-13
* | | Merge PR#441: Port Toplevel to the Stm APIGravatar Maxime Dénès2017-04-12
|\ \ \
| * | | [stm] Remove edit_id.Gravatar Emilio Jesus Gallego Arias2017-04-12
* | | | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...Gravatar Maxime Dénès2017-04-12
|\ \ \ \
* \ \ \ \ Merge PR#532: Clean Nsatz implementation.Gravatar Maxime Dénès2017-04-11
|\ \ \ \ \
* \ \ \ \ \ Merge PR#379: Introducing evar-insensitive constrsGravatar Maxime Dénès2017-04-11
|\ \ \ \ \ \ | |_|_|/ / / |/| | | | |
| | * | | | Fix an algorithmic issue in Nsatz.Gravatar Pierre-Marie Pédrot2017-04-09
| | * | | | Academic prescriptivism strikes back: down with baroque programming in Nsatz.Gravatar Pierre-Marie Pédrot2017-04-09
| |/ / / / |/| | | |
| * | | | Fix an unhandled exception in Omega.Gravatar Pierre-Marie Pédrot2017-04-07
| * | | | Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
| |\ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 20:25:34 +0000