aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
Commit message (Expand)AuthorAge
* [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
* | | Don't use ref universe_opt_substGravatar Gaëtan Gilbert2018-05-08
|/ /
* | [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* | Merge PR #7375: Implement to_constr with nf_evars_and_universes_opt_substGravatar Pierre-Marie Pédrot2018-05-03
|\ \
* \ \ Merge PR #6935: Separate universe minimization and evar normalization functionsGravatar Pierre-Marie Pédrot2018-04-30
|\ \ \
| | * | Implement to_constr with nf_evars_and_universes_opt_substGravatar Gaëtan Gilbert2018-04-29
| | * | Fix nf_evars_universes_opt_subst: recurse on univs, nf undef evarsGravatar Gaëtan Gilbert2018-04-28
| |/ / |/| |
* | | Merge PR #6892: Cleanup implementation of normalize_context_set a bitGravatar Pierre-Marie Pédrot2018-04-28
|\ \ \
* \ \ \ Merge PR #6866: Slight improvement of messages related to direct and indirect...Gravatar Pierre-Marie Pédrot2018-04-25
|\ \ \ \
* \ \ \ \ Merge PR #307: Adding a flag to support different naming modes for evar hypot...Gravatar Pierre-Marie Pédrot2018-04-24
|\ \ \ \ \
| | * | | | Improving error message for clear tactic (and indirect uses of it).Gravatar Hugo Herbelin2018-04-24
| * | | | | Adding a flag to support different naming modes for evar hypotheses.Gravatar Hugo Herbelin2018-04-24
| |/ / / /
* / / / / [api] Relocate `intf` modules according to dependency-order.Gravatar Emilio Jesus Gallego Arias2018-04-23
|/ / / /
| | * / Deprecate mixing univ minimization and evm normalization functions.Gravatar Gaëtan Gilbert2018-04-17
| |/ / |/| |
| * | univ minimization: comment [enforce_uppers]Gravatar Gaëtan Gilbert2018-04-13
| * | univ minimization [enforce_upper]: replace Option.get with matchGravatar Gaëtan Gilbert2018-04-13
| * | univ minimization: Partially let-lift [enforce_uppers]Gravatar Gaëtan Gilbert2018-04-13
| * | univ minimization: rename acc' -> enforce_uppersGravatar Gaëtan Gilbert2018-04-13
| * | univ minimization: use shadowing moreGravatar Gaëtan Gilbert2018-04-13