| Age | Commit message (Expand) | Author |
|---|
| 2013-08-22 | Less "Coq" strings everywhere | letouzey |
| 2013-08-08 | State Transaction Machine | gareuselesinge |
| 2013-08-08 | Side effect free implementation of admit (Isabelle's oracle) | gareuselesinge |
| 2013-08-04 | Fixing #3062. Computation of the value of a fresh identifier was | ppedrot |
| 2013-08-04 | Removing useless casts between arrays and lists. | ppedrot |
| 2013-07-09 | Revising r16550 about providing intro patterns for applying injection: | herbelin |
| 2013-06-05 | Replacing lists by maps in matching interpretation. | ppedrot |
| 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-05-28 | Setting "appcontext" as the default behaviour in Ltac matching. | ppedrot |
| 2013-05-12 | Use the Hook module here and there. | ppedrot |
| 2013-05-09 | A uniformization step around understand_* and interp_* functions. | herbelin |
| 2013-04-29 | Merging Context and Sign. | ppedrot |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-04-25 | raise UnsafeSuccess -> feedback AddedAxiom | gareuselesinge |
| 2013-03-23 | Minor code cleaning in CArray / CList. | ppedrot |
| 2013-03-21 | Using hnf instead of "intro H" for forcing reduction to a product. | herbelin |
| 2013-03-21 | Fixing an old pecularity of "red": head betaiota redexes are now | herbelin |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 10) | letouzey |
| 2013-03-11 | Added a Local Definition vernacular command. This type of definition | ppedrot |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2012-12-21 | Yet a new reduction tactic in Coq : cbn | pboutill |
| 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 | Using library string functions. | ppedrot |
| 2012-11-25 | Monomorphization (tactics) | ppedrot |
| 2012-11-13 | Added a CString module. | ppedrot |
| 2012-11-08 | Monomorphized a lot of equalities over OCaml integers, thanks to | ppedrot |
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 2012-09-18 | More cleaning in CArray... | ppedrot |
| 2012-09-18 | Cleaning interface of Util. | ppedrot |
| 2012-09-17 | More cleaning on Utils and CList. Some parts of the code being | ppedrot |
| 2012-09-14 | As r15801: putting everything from Util.array_* to CArray.*. | 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-09-14 | The new ocaml compiler (4.00) has a lot of very cool warnings, | regisgia |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-07-20 | Reductionops refactoring | pboutill |
| 2012-07-09 | induction/destruct : nicer syntax for generating equations (solves #2741) | letouzey |
| 2012-07-05 | ZArith + other : favor the use of modern names instead of compat notations | letouzey |
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
| 2012-06-01 | Let's try to avoid generating induction principles for records (wish #2693) | letouzey |
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey |
| 2012-05-29 | slim down a bit genarg.ml (pr_intro_pattern forgotten there) | letouzey |
| 2012-05-29 | Glob_term now mli-only, operations now in Glob_ops | letouzey |
| 2012-05-29 | Tacexpr as a mli-only, the few functions there are now in Tacops | letouzey |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
| 2012-04-15 | In "intro until" and its applications, be consistent when reduction is | herbelin |
