aboutsummaryrefslogtreecommitdiff
path: root/pretyping/inductiveops.ml
AgeCommit message (Expand)Author
2018-06-29Merge PR #7080: Swapping Context and Constr and defining declarations on cons...Maxime Dénès
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
2018-06-24Handle mutual records in upper layers.Pierre-Marie Pédrot
2018-06-23Using more general information for primitive records.Pierre-Marie Pédrot
2018-06-19Merge PR #6754: Better elaboration of pattern-matchings on primitive projectionsPierre-Marie Pédrot
2018-06-17Remove the proj_body field from the kernel.Pierre-Marie Pédrot
2018-06-17Remove the proj_eta field of the kernel.Pierre-Marie Pédrot
2018-06-15Better elaboration of pattern-matchings on primitive projectionsMatthieu Sozeau
2018-05-31Reduce circular dependency constants <-> projectionsGaëtan Gilbert
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-02-28[econstr] Continue consolidation of EConstr API under `interp`.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-11Use specialized function for inductive subtyping inference.Gaëtan Gilbert
2018-02-10Inference of inductive subtyping does not need an evar map.Gaëtan Gilbert
2018-02-10Simplification: cumulativity information is variance information.Gaëtan Gilbert
2018-02-10Fix typo in Univ.CumulativityInfoGaëtan Gilbert
2017-12-23[api] Also deprecate constructors of Decl_kinds.Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-09-23Fixing _rect bug for inductive types with let-ins and non-rec uniform params.Hugo Herbelin
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-16Fix a bugAmin Timany
2017-06-16Fix bugsAmin Timany
2017-06-16Subtyping inference for inductoves and recordsAmin Timany
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-01Using delayed universe instances in EConstr.Pierre-Marie Pédrot
2017-04-01Actually exporting delayed universes in the EConstr implementation.Pierre-Marie Pédrot
2017-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Namegen primitives now apply on evar constrs.Pierre-Marie Pédrot
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Introducing contexts parameterized by the inner term type.Pierre-Marie Pédrot
2017-02-14Removing some return type compatibility layers in Termops.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-14Leminv API using EConstr.Pierre-Marie Pédrot
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Unification API using EConstr.Pierre-Marie Pédrot
2017-02-14Cases API using EConstr.Pierre-Marie Pédrot
2017-02-14Retyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2016-12-12Replace Typeops by Fast_typeopsGaetan Gilbert
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-06Fix reopened bug #3317.Matthieu Sozeau
2016-07-06Disallow dependent case on prim records w/o etaMatthieu Sozeau
2016-07-06Renaming to more generic has_dependent_elim testMatthieu Sozeau
2016-07-06Move is_prim... to Inductiveops and correct SchemeMatthieu Sozeau
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 17:51:20 +0000