| Age | Commit message (Expand) | Author |
|---|
| 2013-06-22 | 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-21 | 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-19 | 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-18 | 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-17 | Documenting a potential source of incompleteness in the ring tactic, | amahboub |
| 2013-06-14 | 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-13 | Normalizing exception raised by tactic coercions. | ppedrot |
| 2013-06-12 | 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-10 | Hiding tactic value representations. | ppedrot |
| 2013-06-10 | Fix [setoid_rewrite] forgetting some evars that are produced when typecheckin... | msozeau |
| 2013-06-07 | Cleanup in rewrite.ml4, remove Evd.merge... replaced by an evars_reset_evd | msozeau |
| 2013-06-06 | Fixing bug #3030. | ppedrot |
| 2013-06-06 | Fixing #3056 | ppedrot |
| 2013-06-06 | More comments in Genarg. | ppedrot |
| 2013-06-06 | Uniformizing generic argument types. | ppedrot |
| 2013-06-06 | Document changes and add missing documentation for Program options. | msozeau |
| 2013-06-06 | Add an option to shrink the context of program obligations to avoid | msozeau |
| 2013-06-05 | Replacing lists by maps in matching interpretation. | ppedrot |
| 2013-06-05 | Use a Summary.ref for the tactic in tactic options for proper backtracking | msozeau |
| 2013-06-04 | Backtrack on unneeded change of interface for pose_metas_as_evars. | msozeau |
| 2013-06-04 | Start documenting new [rewrite_strat] tactic that applies rewriting | msozeau |
| 2013-06-02 | A constructive proof of Fan theorem where paths are represented by predicates. | herbelin |
| 2013-06-02 | Making the behavior of "injection ... as ..." more natural: | herbelin |
| 2013-06-02 | Flags V8_4 for compatibility infrastructure. | herbelin |
| 2013-06-02 | Fixing a typo in the documentation of discriminate. | herbelin |
| 2013-06-02 | Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as an | herbelin |
| 2013-06-02 | Fixing buggy backtracking in "intros * pat" with failing "pat". | herbelin |
| 2013-06-02 | Modest protection against "injection" and co raising anomaly in | herbelin |
| 2013-05-30 | Removing a useless location in ltac trace mechanism. | ppedrot |
| 2013-05-30 | Do not compute fallback eagerly in Evarconv | pboutill |
