aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
Commit message (Expand)AuthorAge
...
| | * Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
| |/ |/|
* | Port is_Set and is_Type to EConstr, as was is_Prop already.Gravatar Guillaume Melquiond2017-09-12
| * Normalizing universes before performing term comparison.Gravatar Pierre-Marie Pédrot2017-09-08
| * Using EConstr equality check in unification.Gravatar Pierre-Marie Pédrot2017-09-08
|/
* Merge PR #830: Moving assert (the "Cut" rule) to new proof engineGravatar Maxime Dénès2017-08-29
|\
* \ Merge PR #913: Less allocations in DetypingGravatar Maxime Dénès2017-08-01
|\ \
* \ \ Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\ \ \
| * | | deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* | | | Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
|/ / /
| * / No useless reallocation in Termops.collapse_appl.Gravatar Pierre-Marie Pédrot2017-07-21
|/ /
* | [proofs] Remove circular dependency from Proofview to Goal.Gravatar Emilio Jesus Gallego Arias2017-07-19
* | Merge PR #781: Remove dead code [Universes.simplify_universe_context]Gravatar Maxime Dénès2017-07-17
|\ \
* | | Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.Gravatar Pierre-Marie Pédrot2017-07-13
* | | Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: KernelGravatar Maxime Dénès2017-07-13
|\ \ \
| * | | 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
* | | | Merge PR #816: In enter_one, not having exactly one goal is a fatal error of ...Gravatar Maxime Dénès2017-07-07
|\ \ \ \ | |/ / / |/| | |
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\ \ \ \
* | | | | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| | | | * Adding intermediate entry point to create an evar in empty rel_context.Gravatar Hugo Herbelin2017-06-25
| |_|_|/ |/| | |
| | * | In enter_one, not having exactly one goal is a fatal error of the monad.Gravatar Hugo Herbelin2017-06-23
| |/ / |/| |
| | * Remove dead code [Universes.simplify_universe_context]Gravatar Gaëtan Gilbert2017-06-20
| |/ |/|
* | Merge PR#793: Fixing restriction of existential variables regarding evar_storeGravatar Maxime Dénès2017-06-20
|\ \
* | | Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* | | Squashed commit of the following:Gravatar Amin Timany2017-06-16
* | | Check subtyping of inductive types in KernelGravatar Amin Timany2017-06-16
* | | Using UInfoInd for universes in inductive typesGravatar Amin Timany2017-06-16
* | | New datastructure for universes of inductive typesGravatar Amin Timany2017-06-16
| | * Merge PR#713: Bump year in headers.Gravatar Maxime Dénès2017-06-15
| | |\
| | * \ Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraintsGravatar Maxime Dénès2017-06-15
| | |\ \
| * | | | Fixing restrict regarding evar_store.Gravatar Hugo Herbelin2017-06-14
* | | | | Deprecate options that were introduced for compatibility with 8.4.Gravatar Guillaume Melquiond2017-06-14
* | | | | Remove support for Coq 8.4.Gravatar Guillaume Melquiond2017-06-14
|/ / / /
* | | | Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* | | | Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a sh...Gravatar Maxime Dénès2017-06-06
|\ \ \ \
| | | * | Univs: fix bug #5365, generation of u+k <= v constraintsGravatar Matthieu Sozeau2017-06-05
* | | | | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* | | | | Don't double up on periods in anomaliesGravatar Jason Gross2017-06-02
* | | | | Merge PR#696: Trunk+cleanup constr of globalGravatar Maxime Dénès2017-06-01
|\ \ \ \ \
* \ \ \ \ \ Merge PR#561: Improving the Name APIGravatar Maxime Dénès2017-06-01
|\ \ \ \ \ \
| | | | | | * Bump year in headers.Gravatar Maxime Dénès2017-06-01
| | | | | |/ | | | | |/|
| * | | | | Creating a module Nameops.Name extending module Names.Name.Gravatar Hugo Herbelin2017-05-31
| | | * | | Using EConstr and more invariants in record.ml.Gravatar Hugo Herbelin2017-05-31
| | |/ / / | |/| | |
* / | | | Support for using type information to infer more precise evar sources.Gravatar Hugo Herbelin2017-05-30
|/ / / /
| * / / tactics cleanup: remove constr_of_global callsGravatar Matthieu Sozeau2017-05-29
|/ / /
* | | Merge PR#512: [cleanup] Unify all calls to the error function.Gravatar Maxime Dénès2017-05-29
|\ \ \
| * | | [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* | | | [coqlib] Move `Coqlib` to `library/`.Gravatar Emilio Jesus Gallego Arias2017-05-27
|/ / /
* | | Merge PR#655: Extra functions exported in EConstrGravatar Maxime Dénès2017-05-26
|\ \ \
* \ \ \ Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\ \ \ \