aboutsummaryrefslogtreecommitdiff
path: root/pretyping/reductionops.ml
AgeCommit message (Expand)Author
2017-02-14Ltac now uses evar-based constrs.Pierre-Marie Pédrot
2017-02-14Removing some return type compatibility layers in Termops.Pierre-Marie Pédrot
2017-02-14Cc API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops now return EConstrs.Pierre-Marie Pédrot
2017-02-14Eliminating parts of the right-hand side compatibility layerPierre-Marie Pédrot
2017-02-14Rewrite API using EConstr.Pierre-Marie Pédrot
2017-02-14Inv API using EConstr.Pierre-Marie Pédrot
2017-02-14Clenv API using EConstr.Pierre-Marie Pédrot
2017-02-14Cleaning up opening of the EConstr module in pretyping folder.Pierre-Marie Pédrot
2017-02-14Unification API using EConstr.Pierre-Marie Pédrot
2017-02-14Pretyping 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-10-31Stronger static invariant in equality upto universes.Pierre-Marie Pédrot
2016-10-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-28Remove incorrect assertion in cbn (bug #4822).Guillaume Melquiond
2016-09-14Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-09no-refold patchPaul Steckler
2016-09-08Merge PR #244.Pierre-Marie Pédrot
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19[pp] Fix newline issues.Emilio 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-01Make semantics of whd_zeta consistent with other whd_* functions.Maxime Dénès
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-02Avoid infinite loop/stack overflow when using "simpl nomatch" (bug #4576).Guillaume Melquiond
2016-03-20Making Evarutil independent from Reductionops.Pierre-Marie Pédrot
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-15Using monotonic types for conversion functions.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-12-17CLEANUP: in the Reduction moduleMatej Kosik
2015-12-17CLEANUP: in the Reductionops moduleMatej Kosik
2015-12-17CLEANUP: in the Reduction moduleMatej Kosik
2015-11-26More efficient implementation of equality-up-to-universes in Universes.Pierre-Marie Pédrot
2015-11-22Fixing kernel bug in typing match with let-ins in the arity.Hugo Herbelin
2015-11-09Pushing the backtrace in conversion anomalies.Pierre-Marie Pédrot
2015-10-28Conversion of polymorphic inductive types was incomplete in VM and native.Maxime Dénès
2015-10-15Avoid dependency of the pretyper on C code.Maxime Dénès
2015-10-15 Fix #4346 2/2: VM casts were not inferring universe constraints.Maxime Dénès
2015-10-15Fix #4346 1/2: native casts were not inferring universe constraints.Maxime Dénès
2015-08-02Reverting 16 last commits, committed mistakenly using the wrong push command.Hugo Herbelin
2015-08-02Hopefully clearer printing of stack when debugging evarconv unification.Hugo Herbelin
2015-06-28Fix incompleteness of conversion used by evarconvMatthieu Sozeau
2015-03-04Fix bug #3532, providing universe inconsistency information when aMatthieu Sozeau
2015-03-03Fix bug #4103: forgot to allow unfolding projections of cofixpoints likeMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-19 04:18:18 +0000