aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
...
| | | | * romega: no more normalization trace, replaced by some Coq-side computationGravatar Pierre Letouzey2017-05-22
| | | | * 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
| | |_|/ | |/| |
| | | * Using type classes in the interpretation of "specialize" and "contradiction".Gravatar Hugo Herbelin2017-05-22
| | | * Clarifying the interpretation path for the "constr_with_binding" argument.Gravatar Hugo Herbelin2017-05-22
| | |/ | |/|
| | * Merge branch 'master' into ltac2-hooksGravatar Pierre-Marie Pédrot2017-05-19
| | |\
| * | | 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
| |/ / / /
| | | | * Generalizing the tactic-in-term embedding to any generic argument.Gravatar Pierre-Marie Pédrot2017-05-03
| | | | * Allowing to pass arbitrary data in internalization environments.Gravatar Pierre-Marie Pédrot2017-05-03
| | |_|/ | |/| |
| | | * 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
| |\ \
* | | | [location] [ast] Port module AST to CAstGravatar Emilio Jesus Gallego Arias2017-04-25
* | | | [location] [ast] Switch Constrexpr AST to an extensible node type.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | | | [location] Remove `Loc.internal_ghost`Gravatar Emilio Jesus Gallego Arias2017-04-25
* | | | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* | | | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | | | [location] Use located in tactics.Gravatar Emilio Jesus Gallego Arias2017-04-24
* | | | [location] Use located in misctypes.Gravatar Emilio Jesus Gallego Arias2017-04-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 05:03:47 +0000