aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/reductionops.ml
Commit message (Expand)AuthorAge
* Less footguns in universe handling: remove subst_instance_context.Gravatar Pierre-Marie Pédrot2017-07-11
* Getting rid of simple calls to AUContext.instance.Gravatar Pierre-Marie Pédrot2017-07-11
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
* Squashed commit of the following:Gravatar Amin Timany2017-06-16
* Use inductive subtyping for conv/cumulGravatar Amin Timany2017-06-16
* Merge PR#714: Print feature Proof-of-Concept (episode 2)Gravatar Maxime Dénès2017-06-13
|\
* \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\ \
* | | Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
| | * Added support for a side effect on constants in reduction functions.Gravatar Thomas Sibut-Pinote2017-06-04
* | | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| |/ |/|
* | Merge PR#670: Postponing of universe constraints unification in term equality.Gravatar Maxime Dénès2017-06-01
|\ \
* | | [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* | | [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| * | Postponing of universe constraints unification in term equality.Gravatar Pierre-Marie Pédrot2017-05-23
|/ /
* | Fix 4.04 warningsGravatar Gaetan Gilbert2017-04-27
* | Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
| * Reinstate fixpoint refolding in [cbn], deactivated by mistake.Gravatar Matthieu Sozeau2017-04-13
* | Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
* | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\ \
* | | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Removing some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Cc API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Eliminating parts of the right-hand side compatibility layerGravatar Pierre-Marie Pédrot2017-02-14
* | | Rewrite API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Inv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Clenv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Cleaning up opening of the EConstr module in pretyping folder.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Unification API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Pretyping 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-12-07
|/| | | |/
| * Univs: fix bug #5180Gravatar Matthieu Sozeau2016-11-30
* | Stronger static invariant in equality upto universes.Gravatar Pierre-Marie Pédrot2016-10-31
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\|
| * Remove incorrect assertion in cbn (bug #4822).Gravatar Guillaume Melquiond2016-09-28
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-14
|\|
| * no-refold patchGravatar Paul Steckler2016-09-09
* | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \ | |/ |/|
| * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* | [pp] Fix newline issues.Gravatar 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
* Make semantics of whd_zeta consistent with other whd_* functions.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
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31