| Commit message (Expand) | Author | Age |
... | |
* | Revising r16550 about providing intro patterns for applying injection: | herbelin | 2013-07-09 |
* | Reorganizing intropatterns: * and ** are not naming intropatterns. | herbelin | 2013-07-09 |
* | Fixing a bug in the native compiler, introduced by r16363, leading to undefined | mdenes | 2013-07-06 |
* | Removing SortArgType. | ppedrot | 2013-07-05 |
* | Expurgating the useless difference between List0 and List1 at the | ppedrot | 2013-07-05 |
* | Removing the use of leveled tactics wit_tacticn. It is now handled | ppedrot | 2013-07-02 |
* | Removed the ad-hod handling of wit_tacticn. | ppedrot | 2013-07-02 |
* | Using functors to reduce the boilerplate used in registering | ppedrot | 2013-06-30 |
* | Fixing Camlp4 compilation. | ppedrot | 2013-06-30 |
* | Removed the distinction between generic Ltac vars and Let/Intro | ppedrot | 2013-06-27 |
* | Added a generic handler of Ltac quotations, based on the existing | ppedrot | 2013-06-27 |
* | Getting rid of IntroPatternArgType. | ppedrot | 2013-06-27 |
* | Removing useless tactic arguments, and using generic arguments | ppedrot | 2013-06-27 |
* | Bugfix: Fixing #3050 | ppedrot | 2013-06-27 |
* | Useless use of maps in constr internalizing. | ppedrot | 2013-06-25 |
* | Cleaning up the type of Tacinterp.extract_ltac_constr_values. | ppedrot | 2013-06-24 |
* | Using the whole tactic environment while Pretyping. | ppedrot | 2013-06-24 |
* | Now, idtac closures use maps instead of association list. | ppedrot | 2013-06-22 |
* | Fixing the semantics of the previous patch. | ppedrot | 2013-06-22 |
* | Generalizing the use of maps instead of lists in the interpretation | ppedrot | 2013-06-22 |
* | Splitted up Genarg in four different levels: | ppedrot | 2013-06-21 |
* | Cutting the dependency of Genarg in constr_expr, glob_constr | ppedrot | 2013-06-21 |
* | Revert "KEYID token makes parsing more robust in face of notations" | gareuselesinge | 2013-06-21 |
* | Revert "parse "of" as KEYID "of"" | gareuselesinge | 2013-06-21 |
* | Moving wit_unit to Stdarg. | ppedrot | 2013-06-19 |
* | Adding genarg printer to debugger. | ppedrot | 2013-06-19 |
* | Fixing argument extension. Instead of qualified names, string | ppedrot | 2013-06-19 |
* | - Keep the refinement of existing evars comming from unification with a rewri... | msozeau | 2013-06-19 |
* | parse "of" as KEYID "of" | gareuselesinge | 2013-06-19 |
* | KEYID token makes parsing more robust in face of notations | gareuselesinge | 2013-06-19 |
* | Proof-of-concept: moved four easy-to-handle generic arguments to | ppedrot | 2013-06-18 |
* | Removing the various glob/subst/interp registering functions for | ppedrot | 2013-06-18 |
* | Implementing a new interface for Genarg, with centralized data | ppedrot | 2013-06-18 |
* | Now glob_sign and interp_sign only depend on structures defined | ppedrot | 2013-06-18 |
* | Documenting a potential source of incompleteness in the ring tactic, | amahboub | 2013-06-17 |
* | Exporting field f_debug (needed for Ssreflect). | ppedrot | 2013-06-14 |
* | Using an "extra" Store.t field in interp_sign instead of dedicated | ppedrot | 2013-06-14 |
* | When doing setoid_rewrite through rewrite, do resolution of classes | msozeau | 2013-06-14 |
* | Normalizing exception raised by tactic coercions. | ppedrot | 2013-06-13 |
* | Moving coercion functions out of Tacinterp. | ppedrot | 2013-06-12 |
* | Totally replaced ad-hoc tactic values by generic arguments. Now | ppedrot | 2013-06-12 |
* | Added Genarg as generic argument type. | ppedrot | 2013-06-12 |
* | Changing the type of Ltac values. Now they are toplevel generic | ppedrot | 2013-06-12 |
* | Fixing a Not_found and evar not found anomaly found in ATBR, | msozeau | 2013-06-12 |
* | One more fix for rewrite: disallow resolving of the (partial) constraints | msozeau | 2013-06-12 |
* | Hiding tactic value representations. | ppedrot | 2013-06-10 |
* | Fix [setoid_rewrite] forgetting some evars that are produced when typecheckin... | msozeau | 2013-06-10 |
* | Cleanup in rewrite.ml4, remove Evd.merge... replaced by an evars_reset_evd | msozeau | 2013-06-07 |
* | Fixing bug #3030. | ppedrot | 2013-06-06 |
* | Fixing #3056 | ppedrot | 2013-06-06 |