aboutsummaryrefslogtreecommitdiff
path: root/proofs/redexpr.ml
AgeCommit message (Expand)Author
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-09-06Fixing #8270 (cbn was calling zeta even when not asked for).Hugo Herbelin
2018-06-12[api] Remove Misctypes.Emilio Jesus Gallego Arias
2018-05-31[api] Move `Constrexpr` to the `interp` module.Emilio Jesus Gallego Arias
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
2018-05-23Collecting List.smart_* functions into a module List.Smart.Hugo Herbelin
2018-02-27Update headers following #6543.Théo Zimmermann
2017-12-02[kernel] Patch allowing to disable VM reduction.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-05-24[option] Remove support for non-synchronous options.Emilio Jesus Gallego Arias
2017-04-27Fix omitted labels in function callsGaetan Gilbert
2017-02-14Ltac now uses evar-based constrs.Pierre-Marie Pédrot
2017-02-14Removing compatibility layers in RetypingPierre-Marie Pédrot
2017-02-14Reductionops now return EConstrs.Pierre-Marie Pédrot
2017-02-14Tacred API using EConstr.Pierre-Marie Pédrot
2017-02-14Retyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Nativenorm API using EConstr.Pierre-Marie Pédrot
2017-02-14Vnorm API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2017-02-14Termops API using EConstr.Pierre-Marie Pédrot
2016-09-14Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-09no-refold patchPaul Steckler
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Remove errorlabstrm in favor of user_errEmilio Jesus Gallego Arias
2016-07-03closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Pierre Letouzey
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Add and document match, fix and cofix reduction flags.Maxime Dénès
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-02-15Using monotonic types for conversion functions.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-02Remove some unused functions.Guillaume Melquiond
2015-10-15Fix #4346 1/2: native casts were not inferring universe constraints.Maxime Dénès
2015-05-14Disable precompilation for native_compute by default.Guillaume Melquiond
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-01-18Fix a big bug in native_compute tactic: since Hugo's 364decf59c, it wasMaxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-12-12An option SimplIsCbnPierre Boutillier
2014-12-12Extend the syntax of simpl with a delta flag.Arnaud Spiwack
2014-11-23One more word about "simpl f": avoid "simpl f" to be printed "simpl f",Hugo Herbelin
2014-11-16Enforcing a stronger difference between the two syntaxes "simplHugo Herbelin
2014-10-24Change reduction_of_red_expr to return an e_reduction_function returningMatthieu Sozeau
2014-02-24cbn understands ArgumentsPierre Boutillier
2014-02-24Stack operations of Reductionops in Reductionops.StackPierre Boutillier
2013-12-30Support for evars and metas in native compiler.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:47:55 +0000