| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2013-05-30 | export Unification.abstract_list_all_with_dependencies | pboutill |
| 2013-05-30 | Why not going inside fixpoint definition with appcontext ? | pboutill |
| 2013-05-30 | comments in mli | pboutill |
| 2013-05-30 | bwaa, a Pervasive.compare | pboutill |
| 2013-05-29 | newring.ml4: interp constr arg at interp time (not parse time) | gareuselesinge |
| 2013-05-29 | Make ist (interp_sign) available to TACTIC EXTEND code | gareuselesinge |
| 2013-05-29 | Documenting the "appcontext" by default. | ppedrot |
| 2013-05-29 | More clever implemenation for IStream. | ppedrot |
| 2013-05-28 | Setting "appcontext" as the default behaviour in Ltac matching. | ppedrot |
| 2013-05-28 | Fixing warning of deprecated Argument Scopes. | ppedrot |
| 2013-05-28 | Getting rid of LtacLocated exception transformer. | ppedrot |
| 2013-05-28 | Fixing debug of empty Ltac matching goal. | ppedrot |
| 2013-05-28 | Pushing lazy lists into Ltac. Now, the control flow is explicit | ppedrot |
| 2013-05-28 | Adding a persistent stream data structure. | ppedrot |
| 2013-05-24 | Code cleaning in Matching. | ppedrot |
| 2013-05-23 | Fixing #3042 | ppedrot |
| 2013-05-16 | Fixing Pp.strbrk which was reversing words. | ppedrot |
| 2013-05-16 | std_ppcmds is persistent, errors can be printed twice | gareuselesinge |
| 2013-05-14 | Mini documentation (evar_absorb_arguments). | herbelin |
| 2013-05-14 | Delayed the computation of parameters in sort polymorphism of | herbelin |
| 2013-05-14 | "change ... in ..." and "simpl ... in ..." now consider nested | herbelin |
| 2013-05-14 | Fixing a regression in unification introduced in r16205 (error raised | herbelin |
| 2013-05-14 | Gmap is now useless, hail to Map! | ppedrot |
| 2013-05-14 | Removing the use of Gmap from Auto. | ppedrot |
| 2013-05-14 | Removing Gmap from Classops. Fold order only mattered for printing. | ppedrot |
| 2013-05-14 | Removing useless uses of Gmap. | ppedrot |
| 2013-05-14 | Removing Fmap from libraries, it is not used anymore. | ppedrot |
| 2013-05-14 | Replacing compatibility layer for Fmap in Typeclasses. Code was | ppedrot |
| 2013-05-14 | More semantical-friendly function. | ppedrot |
| 2013-05-14 | Replacing Id.check with Id.is_valid, as its sole use was under | ppedrot |
| 2013-05-12 | Removing Fset, since it is not used anymore. | ppedrot |
| 2013-05-12 | Removing the use of Fset/Fmap from Trie. There was actually only | ppedrot |
| 2013-05-12 | Documenting the previous commit. | ppedrot |
| 2013-05-12 | Granting wish #3014: | ppedrot |
| 2013-05-12 | Removing Gmap from Extraction plugin | ppedrot |
| 2013-05-12 | Use the Hook module here and there. | ppedrot |
| 2013-05-12 | Added a generic notion of hook. Hooks are functions to be set | ppedrot |
| 2013-05-11 | Fixing a source of evars leak, revealed by contrib QuicksortComplexity | herbelin |
| 2013-05-10 | Removing Gmap from Tacinterp. | ppedrot |
| 2013-05-10 | Little oversight in commit r16489 (fix for bug #3036). | herbelin |
| 2013-05-09 | Documenting the Tries module, uniformizing the names according to | ppedrot |
