aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/inductiveops.ml
Commit message (Expand)AuthorAge
* Merge PR #7080: Swapping Context and Constr and defining declarations on cons...Gravatar Maxime Dénès2018-06-29
|\
| * Swapping Context and Constr: defining declarations on constr in Constr.Gravatar Hugo Herbelin2018-06-27
* | Handle mutual records in upper layers.Gravatar Pierre-Marie Pédrot2018-06-24
|/
* Using more general information for primitive records.Gravatar Pierre-Marie Pédrot2018-06-23
* Merge PR #6754: Better elaboration of pattern-matchings on primitive projectionsGravatar Pierre-Marie Pédrot2018-06-19
|\
* | Remove the proj_body field from the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
* | Remove the proj_eta field of the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
| * Better elaboration of pattern-matchings on primitive projectionsGravatar Matthieu Sozeau2018-06-15
|/
* Reduce circular dependency constants <-> projectionsGravatar Gaëtan Gilbert2018-05-31
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-02-28
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* Use specialized function for inductive subtyping inference.Gravatar Gaëtan Gilbert2018-02-11
* Inference of inductive subtyping does not need an evar map.Gravatar Gaëtan Gilbert2018-02-10
* Simplification: cumulativity information is variance information.Gravatar Gaëtan Gilbert2018-02-10
* Fix typo in Univ.CumulativityInfoGravatar Gaëtan Gilbert2018-02-10
* [api] Also deprecate constructors of Decl_kinds.Gravatar Emilio Jesus Gallego Arias2017-12-23
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Fixing _rect bug for inductive types with let-ins and non-rec uniform params.Gravatar Hugo Herbelin2017-09-23
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Fix a bugGravatar Amin Timany2017-06-16
* Fix bugsGravatar Amin Timany2017-06-16
* Subtyping inference for inductoves and recordsGravatar Amin Timany2017-06-16
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
* Actually exporting delayed universes in the EConstr implementation.Gravatar Pierre-Marie Pédrot2017-04-01
* Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\
* | Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* | Introducing contexts parameterized by the inner term type.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing some return type compatibility layers in Termops.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
* | Leminv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Unification API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Cases API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Retyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| * Replace Typeops by Fast_typeopsGravatar Gaetan Gilbert2016-12-12
|/
* 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
* Fix reopened bug #3317.Gravatar Matthieu Sozeau2016-07-06
* Disallow dependent case on prim records w/o etaGravatar Matthieu Sozeau2016-07-06
* Renaming to more generic has_dependent_elim testGravatar Matthieu Sozeau2016-07-06
* Move is_prim... to Inductiveops and correct SchemeGravatar Matthieu Sozeau2016-07-06
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 19:37:56 +0000