| Age | Commit message (Expand) | Author |
|---|
| 2013-11-02 | Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations. | aspiwack |
| 2013-11-02 | Getting rid of Goal.here, and all the related exceptions and combinators. | aspiwack |
| 2013-11-02 | Uses Proofview.tclEXTEND more sparingly. | aspiwack |
| 2013-11-02 | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack |
| 2013-10-24 | More monomorphic List.mem + List.assoc + ... | letouzey |
| 2013-10-23 | cList: set-as-list functions are now with an explicit comparison | letouzey |
| 2013-10-05 | Moving side effects into evar_map. There was no reason to keep another | ppedrot |
| 2013-09-19 | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc |
| 2013-09-18 | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot |
| 2013-09-03 | Some cleanup in Auto | ppedrot |
| 2013-08-28 | Removing some lone List.assoc & List.mem in lib. | ppedrot |
| 2013-08-08 | State Transaction Machine | gareuselesinge |
| 2013-08-03 | Small fixes due to the arrival of OCaml 3.12. | ppedrot |
| 2013-07-17 | Pre-create typeclass_instances and rewrite hintdb in Auto | letouzey |
| 2013-06-05 | Replacing lists by maps in matching interpretation. | ppedrot |
| 2013-05-14 | Removing the use of Gmap from Auto. | ppedrot |
| 2013-05-12 | Use the Hook module here and there. | ppedrot |
| 2013-05-06 | States: frozen states can hold closures | gareuselesinge |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-03-23 | Minor code cleaning in CArray / CList. | ppedrot |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 11) | letouzey |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2012-12-18 | Fixed a little inefficiency of "set/destruct" over a pattern. Now | herbelin |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-12-14 | Moved Intset and Intmap to Int namespace. | ppedrot |
| 2012-12-13 | Renamed Option.Misc.compare to the more uniform Option.equal. | ppedrot |
| 2012-12-08 | Finish patch for Hint Resolve, stopping to generate new constant names for | msozeau |
| 2012-11-25 | Monomorphization (tactics) | ppedrot |
| 2012-11-08 | Monomorphized a lot of equalities over OCaml integers, thanks to | ppedrot |
| 2012-10-31 | Change [Hints Resolve] to still accept constrs as arguments | msozeau |
| 2012-10-26 | Change Hint Resolve, Immediate to take a global reference as argument | msozeau |
| 2012-10-06 | still some more dead code removal | letouzey |
| 2012-10-06 | remove Refiner.abstract_tactic and similar | letouzey |
| 2012-10-06 | Clean-up : removal of Proof_type.tactic_expr | letouzey |
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 2012-09-17 | More cleaning on Utils and CList. Some parts of the code being | ppedrot |
| 2012-09-14 | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot |
| 2012-09-14 | This patch removes unused "open" (automatically generated from | regisgia |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-08-05 | Dump references | pboutill |
| 2012-07-06 | Fix order of introduction of hints to preserve most-recent-first semantics. | msozeau |
| 2012-06-28 | Fixing previous commit. | ppedrot |
| 2012-06-28 | Fixing info_auto / info_trivial display. | ppedrot |
| 2012-06-04 | Forward-port fixes from 8.4 (15358, 15353, 15333). | msozeau |
| 2012-05-30 | Getting rid of Pp.msg | ppedrot |
| 2012-05-30 | More uniformisation in Pp.warn functions. | ppedrot |
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey |
| 2012-05-29 | Pattern as a mli-only file, operations in Patternops | letouzey |
| 2012-05-29 | New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr | letouzey |
| 2012-05-29 | Glob_term now mli-only, operations now in Glob_ops | letouzey |
