| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-01-02 | Use streams rather than strings to handle bullet suggestions. | Guillaume Melquiond | |
| 2016-01-02 | Remove some unused functions. | Guillaume Melquiond | |
| Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot. | |||
| 2016-01-02 | Remove keys for evar and meta, since they cannot occur. | Guillaume Melquiond | |
| 2016-01-02 | Remove some useless type declarations. | Guillaume Melquiond | |
| 2016-01-02 | Remove some useless module opening. | Guillaume Melquiond | |
| 2016-01-02 | Remove duplicate definition. | Guillaume Melquiond | |
| 2016-01-02 | Remove duplicate declarations. | Guillaume Melquiond | |
| 2016-01-02 | Reduce dependencies of interface files. | Guillaume Melquiond | |
| 2016-01-02 | Avoid warnings about loop indices. | Guillaume Melquiond | |
| 2016-01-02 | Remove useless rec flags. | Guillaume Melquiond | |
| 2016-01-02 | Simplification of grammar_prod_item type. | Pierre-Marie Pédrot | |
| Actually the identifier was never used and just carried along. | |||
| 2016-01-02 | Proper datatype for EXTEND syntax tokens. | Pierre-Marie Pédrot | |
| 2016-01-02 | Separation of concern in TacAlias API. | Pierre-Marie Pédrot | |
| The TacAlias node now only contains the arguments fed to the tactic notation. The binding variables are worn by the tactic representation in Tacenv. | |||
| 2016-01-01 | Fix typos. | Guillaume Melquiond | |
| 2016-01-01 | Remove unused hashconsing code. | Guillaume Melquiond | |
| 2016-01-01 | Do not make it harder on the compiler optimizer by packing arguments. | Guillaume Melquiond | |
| 2016-01-01 | Remove unused functions. | Guillaume Melquiond | |
| 2016-01-01 | Remove unplugged button from the interface. | Guillaume Melquiond | |
| 2016-01-01 | Remove useless recursive flags. | Guillaume Melquiond | |
| 2016-01-01 | Remove unused open. | Guillaume Melquiond | |
| 2016-01-01 | Remove duplicate declarations. | Guillaume Melquiond | |
| 2015-12-31 | Remove unused function Checker.print_loc. | Guillaume Melquiond | |
| There is no location to print anyway, so it will never be useful. | |||
| 2015-12-31 | Merge branch 'v8.5' into trunk | Guillaume Melquiond | |
| 2015-12-31 | Do not compose List.length with List.filter. | Guillaume Melquiond | |
| 2015-12-31 | Remove Library.mem, which is pointless since 8.5. | Guillaume Melquiond | |
| 2015-12-31 | Do not dump a glob reference when its location is ghost. (Fix bug #4469) | Guillaume Melquiond | |
| This patch also causes the code to finish a bit faster in the NoGlob case by not preparing a string for dump_string. It also optimizes Dumpglob.is_ghost by only checking whether the end position is zero. Note that no ghost locations were part of the glob files of the standard library before the patch. Note also that the html documentation of the standard library is bitwise identical before and after the patch. | |||
| 2015-12-30 | Moving apply_type to new proof engine. | Hugo Herbelin | |
| Note that code depending on apply_type might now have to ensure that typing constraints that were possibly generated by apply_type are now taken into account in advance. | |||
| 2015-12-30 | Taking into account generated typing constraints in tactic "generalize". | Hugo Herbelin | |
| 2015-12-30 | Simplifying code of fourier. | Hugo Herbelin | |
| 2015-12-30 | External tactics and notations now accept any tactic argument. | Pierre-Marie Pédrot | |
| This commit has deep consequences in term of tactic evaluation, as it allows to pass any tac_arg to ML and alias tactics rather than mere generic arguments. This makes the evaluation much more uniform, and in particular it removes the special evaluation function for notations. This last point may break some notations out there unluckily. I had to treat in an ad-hoc way the tactic(...) entry of tactic notations because it is actually not interpreted as a generic argument but rather as a proper tactic expression instead. There is for now no syntax to pass any tactic argument to a given ML or notation tactic, but this should come soon. Also fixes bug #3849 en passant. | |||
| 2015-12-29 | Fixing bug #4462: unshelve: Anomaly: Uncaught exception Not_found. | Pierre-Marie Pédrot | |
| The rewrite tactic was causing an evar leak because of the use of the Evd.remove primitive. This function did not modify the future goals of the evarmap to remove the considered evar and thus maintained dangling evars in there, causing the anomaly. | |||
| 2015-12-28 | Removing unused parsing entries. | Pierre-Marie Pédrot | |
| 2015-12-28 | Implementing non-focussed generic arguments. | Pierre-Marie Pédrot | |
| Kind of enhances the situation of bug #4409. Now arguments can be interpreted globally or focussedly in a dynamic fashion because the interpretation function returns a Ftactic.t. The bug is not fixed yet because we should tweak the interpretation of tactic arguments. | |||
| 2015-12-28 | Removing the special status of open_constr generic argument. | Pierre-Marie Pédrot | |
| We also intepret it at toplevel as a true constr and push the resulting evarmap in the current state. | |||
| 2015-12-28 | Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr. | Pierre-Marie Pédrot | |
| 2015-12-27 | Factorizing code for untyped constr evaluation. | Pierre-Marie Pédrot | |
| 2015-12-27 | Removing dead code. | Pierre-Marie Pédrot | |
| 2015-12-27 | Tentative API fix for tactic arguments to be fed to tclWITHHOLES. | Pierre-Marie Pédrot | |
| The previous implementation was a source of evar leaks if misused, as it created values coming together with their current evar_map. This is dead wrong if the value is not used on the spot. To fix this, we rather return a ['a delayed_open] object. Two argument types were modified: bindings and constr_bindings. The open_constr argument should also be fixed, but it is more entangled and thus I leave it for another commit. | |||
| 2015-12-25 | Moving basic generalization tactics upwards for possible use in "intros". | Hugo Herbelin | |
| 2015-12-25 | Moving code of specialize so that it can accept "as" (no semantic change). | Hugo Herbelin | |
| 2015-12-25 | Moving specialize to Proofview.tactic. | Hugo Herbelin | |
| 2015-12-25 | Fixing a bug in the order of side conditions for introduction pattern -> and <-. | Hugo Herbelin | |
| 2015-12-25 | Fixing an "injection as" bug in the presence of side conditions. | Hugo Herbelin | |
| 2015-12-25 | Moving the ad hoc interpretation of "intros" as "intros **" from tacinterp.ml | Hugo Herbelin | |
| to g_tactic.ml4 so as to leave room for "IntroPattern []" to mean "no introduction". | |||
| 2015-12-25 | Fixing non exhaustive pattern-matching in 003fe3d5e60b. | Hugo Herbelin | |
| 2015-12-24 | Removing auto from the tactic AST. | Pierre-Marie Pédrot | |
| 2015-12-24 | Removing the last quoted auto tactic in Tauto. | Pierre-Marie Pédrot | |
| 2015-12-23 | Partial backtrack on commit 20641795624. | Pierre-Marie Pédrot | |
| The parsing rules were broken and disallowed tactic replacement of the form Ltac ident ::= expr. | |||
| 2015-12-22 | Avoid a pointless conversion/copy. | Guillaume Melquiond | |
| 2015-12-22 | Do not compose "str" and "to_string" whenever possible. | Guillaume Melquiond | |
| For instance, calling only Id.print is faster than calling both str and Id.to_string, since the latter performs a copy. It also makes the code a bit simpler to read. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |