aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
Commit message (Expand)AuthorAge
* change into QuestionMark defaultGravatar Siddharth Bhat2018-07-17
* Change QuestionMark for better record field missing error message.Gravatar Siddharth Bhat2018-07-17
* Evarutil.(e_)new_Type: remove unused env argumentGravatar Gaëtan Gilbert2018-07-03
* Remove unused function Evd.whd_sort_variableGravatar Gaëtan Gilbert2018-07-03
* Remove unused output of Universes.normalize_univ_variablesGravatar Gaëtan Gilbert2018-07-03
* Remove unused env argument to fresh_sort_in_familyGravatar Gaëtan Gilbert2018-07-03
* Swapping Context and Constr: defining declarations on constr in Constr.Gravatar Hugo Herbelin2018-06-27
* Merge PR #7863: Remove Sorts.contentsGravatar Pierre-Marie Pédrot2018-06-27
|\
* \ Merge PR #7826: evd: restrict_evar with candidates, can raise NoCandidatesLeftGravatar Hugo Herbelin2018-06-26
|\ \
* \ \ Merge PR #7906: universes_of_constr don't include universes of monomorphic co...Gravatar Pierre-Marie Pédrot2018-06-26
|\ \ \
| | | * Remove Sorts.contentsGravatar Gaëtan Gilbert2018-06-26
| |_|/ |/| |
| * | universes_of_constr don't include universes of monomorphic constantsGravatar Gaëtan Gilbert2018-06-26
* | | Merge PR #7827: [engine] safe [add_unification_pb] interfaceGravatar Pierre-Marie Pédrot2018-06-23
|\ \ \ | |/ / |/| |
* | | Merge PR #7797: Remove reference name type.Gravatar Enrico Tassi2018-06-19
|\ \ \
* | | | Fix #7421: constr_eq ignores universe constraints.Gravatar Gaëtan Gilbert2018-06-18
| * | | Remove reference name type.Gravatar Maxime Dénès2018-06-18
|/ / /
| | * evd: restrict_evar with candidates, can raise NoCandidatesLeftGravatar Matthieu Sozeau2018-06-15
| |/ |/|
| * evd/evarutil: safe [add_unification_pb] interface, taking EConstr'sGravatar Matthieu Sozeau2018-06-15
|/
* [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Misctypes removal: miscellaneous aliases.Gravatar Emilio Jesus Gallego Arias2018-06-12
* Add a bit of doc to EConstr.decompose_lam*Gravatar Gaëtan Gilbert2018-06-08
* Merge PR #7706: Fix wrong deprecation msgGravatar Pierre-Marie Pédrot2018-06-07
|\
* \ Merge PR #6874: [econstr] Some minor tweaksGravatar Pierre-Marie Pédrot2018-06-07
|\ \
| | * Update evarutil.mliGravatar Matthieu Sozeau2018-06-05
| | * Fix wrong deprecation msgGravatar Matthieu Sozeau2018-06-05
| |/ |/|
* | Merge PR #7495: Fix restrict_universe_contextGravatar Matthieu Sozeau2018-06-05
|\ \
| | * [econstr] Remove some Unsafe.to_constr use.Gravatar Emilio Jesus Gallego Arias2018-06-04
| | * [termops] Update type of function, anyways not used in the codebase.Gravatar Emilio Jesus Gallego Arias2018-06-04
| |/ |/|
* | Merge PR #7216: Replace uses of Termops.dependent by more specific functions.Gravatar Matthieu Sozeau2018-06-04
|\ \
* | | [api] Move `Constrexpr` to the `interp` module.Gravatar Emilio Jesus Gallego Arias2018-05-31
* | | [api] Remove deprecated objects in engine / interp / libraryGravatar Emilio Jesus Gallego Arias2018-05-30
* | | [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
| | * Fix restrict_universe_contextGravatar Gaëtan Gilbert2018-05-30
| |/ |/|
* | Merge PR #7521: Fix soundness bug with VM/native and cofixpointsGravatar Pierre-Marie Pédrot2018-05-28
|\ \
| * | Unify pre_env and envGravatar Maxime Dénès2018-05-28
* | | Remove some occurrences of Evd.emptyGravatar Maxime Dénès2018-05-25
|/ /
* | Collecting Map.smart_* functions into a module Map.Smart.Gravatar Hugo Herbelin2018-05-23
* | Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.Gravatar Hugo Herbelin2018-05-23
* | Collecting Array.smart_* functions into a module Array.Smart.Gravatar Hugo Herbelin2018-05-23
* | Split off Universes functions for minimization.Gravatar Gaëtan Gilbert2018-05-17
* | Make Universes.refresh_constraints internal to UStateGravatar Gaëtan Gilbert2018-05-17
* | Split off Universes functions about substitutions and constraintsGravatar Gaëtan Gilbert2018-05-17
* | Move solve_constraint_system near its only use site (comInductive)Gravatar Gaëtan Gilbert2018-05-17
* | Split off Universes functions dealing with generating new universes.Gravatar Gaëtan Gilbert2018-05-17
* | Split off Universes functions dealing with names.Gravatar Gaëtan Gilbert2018-05-17
* | Make set minimization option internal to UniversesGravatar Gaëtan Gilbert2018-05-17
* | Merge PR #7359: Reduce usage of evar_map referencesGravatar Pierre-Marie Pédrot2018-05-17
|\ \
| * | Use evd_combX in Cases.Gravatar Gaëtan Gilbert2018-05-14
| * | Convert clear_hyps_in_evi to state passing style.Gravatar Gaëtan Gilbert2018-05-11
| * | Deprecate most evarutil evdref functionsGravatar Gaëtan Gilbert2018-05-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-21 10:37:09 +0000