aboutsummaryrefslogtreecommitdiff
path: root/engine
AgeCommit message (Expand)Author
2018-06-18Fix #7421: constr_eq ignores universe constraints.Gaëtan Gilbert
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: miscellaneous aliases.Emilio Jesus Gallego Arias
2018-06-08Add a bit of doc to EConstr.decompose_lam*Gaëtan Gilbert
2018-06-07Merge PR #7706: Fix wrong deprecation msgPierre-Marie Pédrot
2018-06-07Merge PR #6874: [econstr] Some minor tweaksPierre-Marie Pédrot
2018-06-05Update evarutil.mliMatthieu Sozeau
2018-06-05Fix wrong deprecation msgMatthieu Sozeau
2018-06-05Merge PR #7495: Fix restrict_universe_contextMatthieu Sozeau
2018-06-04[econstr] Remove some Unsafe.to_constr use.Emilio Jesus Gallego Arias
2018-06-04[termops] Update type of function, anyways not used in the codebase.Emilio Jesus Gallego Arias
2018-06-04Merge PR #7216: Replace uses of Termops.dependent by more specific functions.Matthieu Sozeau
2018-05-31[api] Move `Constrexpr` to the `interp` module.Emilio Jesus Gallego Arias
2018-05-30[api] Remove deprecated objects in engine / interp / libraryEmilio Jesus Gallego Arias
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
2018-05-30Fix restrict_universe_contextGaëtan Gilbert
2018-05-28Merge PR #7521: Fix soundness bug with VM/native and cofixpointsPierre-Marie Pédrot
2018-05-28Unify pre_env and envMaxime Dénès
2018-05-25Remove some occurrences of Evd.emptyMaxime Dénès
2018-05-23Collecting Map.smart_* functions into a module Map.Smart.Hugo Herbelin
2018-05-23Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.Hugo Herbelin
2018-05-23Collecting Array.smart_* functions into a module Array.Smart.Hugo Herbelin
2018-05-17Split off Universes functions for minimization.Gaëtan Gilbert
2018-05-17Make Universes.refresh_constraints internal to UStateGaëtan Gilbert
2018-05-17Split off Universes functions about substitutions and constraintsGaëtan Gilbert
2018-05-17Move solve_constraint_system near its only use site (comInductive)Gaëtan Gilbert
2018-05-17Split off Universes functions dealing with generating new universes.Gaëtan Gilbert
2018-05-17Split off Universes functions dealing with names.Gaëtan Gilbert
2018-05-17Make set minimization option internal to UniversesGaëtan Gilbert
2018-05-17Merge PR #7359: Reduce usage of evar_map referencesPierre-Marie Pédrot
2018-05-14Use evd_combX in Cases.Gaëtan Gilbert
2018-05-11Convert clear_hyps_in_evi to state passing style.Gaëtan Gilbert
2018-05-11Deprecate most evarutil evdref functionsGaëtan Gilbert
2018-05-08Don't use ref universe_opt_substGaëtan Gilbert
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-05-03Merge PR #7375: Implement to_constr with nf_evars_and_universes_opt_substPierre-Marie Pédrot
2018-04-30Merge PR #6935: Separate universe minimization and evar normalization functionsPierre-Marie Pédrot
2018-04-29Implement to_constr with nf_evars_and_universes_opt_substGaëtan Gilbert
2018-04-28Fix nf_evars_universes_opt_subst: recurse on univs, nf undef evarsGaëtan Gilbert
2018-04-28Merge PR #6892: Cleanup implementation of normalize_context_set a bitPierre-Marie Pédrot
2018-04-25Merge PR #6866: Slight improvement of messages related to direct and indirect...Pierre-Marie Pédrot
2018-04-24Merge PR #307: Adding a flag to support different naming modes for evar hypot...Pierre-Marie Pédrot
2018-04-24Improving error message for clear tactic (and indirect uses of it).Hugo Herbelin
2018-04-24Adding a flag to support different naming modes for evar hypotheses.Hugo Herbelin
2018-04-23[api] Relocate `intf` modules according to dependency-order.Emilio Jesus Gallego Arias
2018-04-17Deprecate mixing univ minimization and evm normalization functions.Gaëtan Gilbert
2018-04-13univ minimization: comment [enforce_uppers]Gaëtan Gilbert
2018-04-13univ minimization [enforce_upper]: replace Option.get with matchGaëtan Gilbert
2018-04-13univ minimization: Partially let-lift [enforce_uppers]Gaëtan Gilbert
2018-04-13univ minimization: rename acc' -> enforce_uppersGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:01:40 +0000