aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/redexpr.ml
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [kernel] Patch allowing to disable VM reduction.Gravatar Emilio Jesus Gallego Arias2017-12-02
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
* Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
* Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
* Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Tacred API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Retyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Nativenorm API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Vnorm API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-14
|\
| * no-refold patchGravatar Paul Steckler2016-09-09
* | Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* | Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
|/
* closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Add and document match, fix and cofix reduction flags.Gravatar Maxime Dénès2016-07-01
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Using monotonic types for conversion functions.Gravatar Pierre-Marie Pédrot2016-02-15
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Remove some unused functions.Gravatar Guillaume Melquiond2016-01-02
|/
* Fix #4346 1/2: native casts were not inferring universe constraints.Gravatar Maxime Dénès2015-10-15
* Disable precompilation for native_compute by default.Gravatar Guillaume Melquiond2015-05-14
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Fix a big bug in native_compute tactic: since Hugo's 364decf59c, it wasGravatar Maxime Dénès2015-01-18
* Update headers.Gravatar Maxime Dénès2015-01-12
* An option SimplIsCbnGravatar Pierre Boutillier2014-12-12
* Extend the syntax of simpl with a delta flag.Gravatar Arnaud Spiwack2014-12-12
* One more word about "simpl f": avoid "simpl f" to be printed "simpl f",Gravatar Hugo Herbelin2014-11-23
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
* Change reduction_of_red_expr to return an e_reduction_function returningGravatar Matthieu Sozeau2014-10-24
* cbn understands ArgumentsGravatar Pierre Boutillier2014-02-24
* Stack operations of Reductionops in Reductionops.StackGravatar Pierre Boutillier2014-02-24
* Support for evars and metas in native compiler.Gravatar Maxime Dénès2013-12-30
* Fixing bug #3169 and avoiding anomaly in bug #2885 (vm_compute notGravatar Hugo Herbelin2013-11-29
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
* code simplifications concerning SummaryGravatar letouzey2013-04-22
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Reductionops: whd_state_gen can take and answers a cst_stack tooGravatar pboutill2013-01-24
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Yet a new reduction tactic in Coq : cbnGravatar pboutill2012-12-21