aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* romega/const_omega : a few improvements (less try with, no gen equality)Gravatar Pierre Letouzey2017-05-22
* romega: use N instead of nat for TvarGravatar Pierre Letouzey2017-05-22
* romega: shorter trace (no more term lengths)Gravatar Pierre Letouzey2017-05-22
* refl_omega: refactoring of normalize_equationGravatar Pierre Letouzey2017-05-22
* ReflOmegaCore: lots of dead code + a few refactored proofsGravatar Pierre Letouzey2017-05-22
* romega: if it bugs again, at least do it with a short and quick errorGravatar Pierre Letouzey2017-05-22
* refl_omega: comment the lack of lifts when dealing with arrowsGravatar Pierre Letouzey2017-05-22
* romega: discard constructor D_mono (shorter trace + fix a bug)Gravatar Pierre Letouzey2017-05-22
* refl_omega: more refactoring (e.g. IntSets instead of sorted lists)Gravatar Pierre Letouzey2017-05-22
* refl_omega: refactoring (e.g. useless args in destructurate_pos_hyp)Gravatar Pierre Letouzey2017-05-22
* ReflOmegaCore: discard useless cosntructor P_NOPGravatar Pierre Letouzey2017-05-22
* ReflOmegaCore: revised proofs (mostly bullets instead of ;[|||])Gravatar Pierre Letouzey2017-05-22
* 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
| |/ / |/| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 07:24:16 +0000