| Age | Commit message (Expand) | Author |
|---|
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 13) | letouzey |
| 2013-03-11 | Allowing (Co)Fixpoint to be defined local and Let-style. | ppedrot |
| 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-14 | Modulification of identifier | ppedrot |
| 2012-12-14 | Moved Intset and Intmap to Int namespace. | ppedrot |
| 2012-12-14 | Implemented a full-fledged equality on [constr_expr]. By the way, | ppedrot |
| 2012-11-26 | Monomorphization (toplevel) | 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 | Cleaning interface of Util. | ppedrot |
| 2012-09-15 | Some documentation and cleaning of CList and Util interfaces. | ppedrot |
| 2012-09-14 | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot |
| 2012-09-14 | The new ocaml compiler (4.00) has a lot of very cool warnings, | regisgia |
| 2012-09-06 | Fix computation of obligations for mutually recursive definitions. | msozeau |
| 2012-08-24 | Assumption commands are now displayed as unsafe in Coqide. | aspiwack |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-07-12 | Bug 2838: ExplApp in mutual inductive parameters | pboutill |
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
| 2012-06-04 | Fixing previous commit (something strange happened...) | ppedrot |
| 2012-06-04 | Replacing some str with strbrk | ppedrot |
| 2012-06-04 | Separated notice vs info messages, and cleaned up the interface a bit. | ppedrot |
| 2012-06-04 | Forward-port fixes from 8.4 (15358, 15353, 15333). | msozeau |
| 2012-06-01 | Cleaning Pp.ppnl use | 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 | Basic stuff about constr_expr migrated from topconstr to constrexpr_ops | letouzey |
| 2012-05-29 | New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr | letouzey |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
| 2012-05-29 | Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd | letouzey |
| 2012-04-27 | Implicit arguments of Definition are taken from the type when given by the user. | pboutill |
| 2012-04-17 | Bug 2733 : { } implicits and Fixpoints | pboutill |
| 2012-03-20 | Fix interface of resolve_typeclasses: onlyargs -> with_goals: | msozeau |
| 2012-03-20 | Continuing r15045-15046 and r15055 (fixing bug #2732 about atomic | herbelin |
| 2012-03-19 | Fix bugs related to Program integration. | msozeau |
| 2012-03-14 | Final part of moving Program code inside the main code. Adapted add_definitio... | msozeau |
| 2012-03-14 | Integrated obligations/eterm and program well-founded fixpoint building to to... | msozeau |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-12-17 | A pass on warning printings. Made systematic the use of msg_warning so | herbelin |
| 2011-12-12 | Proof using ... | gareuselesinge |
| 2011-11-17 | Merge subinstances branch by me and Tom Prince. | msozeau |
| 2011-10-11 | Various simplifications about constant_of_delta and mind_of_delta | letouzey |
| 2011-04-13 | Revert "Add [Polymorphic] flag for defs" | msozeau |
| 2011-04-13 | Add [Polymorphic] flag for defs | msozeau |
| 2011-02-10 | Fixpoints are traverse during implicits arguments search to toplevel | pboutill |
| 2011-02-10 | Interp a definition with the implicit arguments of its local context | pboutill |
| 2011-01-28 | Remove the "Boxed" syntaxes and the const_entry_boxed field | letouzey |
| 2010-12-24 | More {raw => glob} changes for consistency | glondu |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
