| Age | Commit message (Expand) | Author |
|---|
| 2016-09-09 | no-refold patch | Paul Steckler |
| 2016-07-03 | closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module) | Pierre Letouzey |
| 2016-07-03 | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod... | Pierre Letouzey |
| 2016-07-01 | Add and document match, fix and cofix reduction flags. | Maxime Dénès |
| 2016-07-01 | Separate flags for fix/cofix/match reduction and clean reduction function names. | Maxime Dénès |
| 2016-06-29 | A new infrastructure for warnings. | Maxime Dénès |
| 2016-05-31 | Feedback cleanup | Emilio Jesus Gallego Arias |
| 2016-02-15 | Using monotonic types for conversion functions. | Pierre-Marie Pédrot |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2016-01-02 | Remove some unused functions. | Guillaume Melquiond |
| 2015-10-15 | Fix #4346 1/2: native casts were not inferring universe constraints. | Maxime Dénès |
| 2015-05-14 | Disable precompilation for native_compute by default. | Guillaume Melquiond |
| 2015-04-23 | Remove almost all the uses of string concatenation when building error messages. | Guillaume Melquiond |
| 2015-01-18 | Fix a big bug in native_compute tactic: since Hugo's 364decf59c, it was | Maxime Dénès |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-12-12 | An option SimplIsCbn | Pierre Boutillier |
| 2014-12-12 | Extend the syntax of simpl with a delta flag. | Arnaud Spiwack |
| 2014-11-23 | One more word about "simpl f": avoid "simpl f" to be printed "simpl f", | Hugo Herbelin |
| 2014-11-16 | Enforcing a stronger difference between the two syntaxes "simpl | Hugo Herbelin |
| 2014-10-24 | Change reduction_of_red_expr to return an e_reduction_function returning | Matthieu Sozeau |
| 2014-02-24 | cbn understands Arguments | Pierre Boutillier |
| 2014-02-24 | Stack operations of Reductionops in Reductionops.Stack | Pierre Boutillier |
| 2013-12-30 | Support for evars and metas in native compiler. | Maxime Dénès |
| 2013-11-29 | Fixing bug #3169 and avoiding anomaly in bug #2885 (vm_compute not | Hugo Herbelin |
| 2013-10-31 | Conv_orable made functional and part of pre_env | gareuselesinge |
| 2013-04-22 | code simplifications concerning Summary | letouzey |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2013-01-24 | Reductionops: whd_state_gen can take and answers a cst_stack too | pboutill |
| 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-14 | Modulification of identifier | ppedrot |
| 2012-12-14 | Moved Stringset and Stringmap to String namespace. | ppedrot |
| 2012-11-25 | Monomorphization (proof) | ppedrot |
| 2012-09-14 | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot |
| 2012-08-08 | Updating headers. | herbelin |
| 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 | Glob_term now mli-only, operations now in Glob_ops | letouzey |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
| 2012-03-02 | Noise for nothing | pboutill |
| 2012-01-30 | Added an pattern / occurence syntax for vm_compute. | ppedrot |
| 2011-11-02 | Add type annotations around all calls to Libobject.declare_object | letouzey |
| 2011-04-03 | Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks | letouzey |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-01-28 | New command Declare Reduction <id> := <conv_expr>. | letouzey |
| 2009-12-24 | In "simpl c" and "change c with d", c can be a pattern. | herbelin |
