aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evarutil.mli
Commit message (Expand)AuthorAge
* Evarutil.(e_)new_Type: remove unused env argumentGravatar Gaëtan Gilbert2018-07-03
* Swapping Context and Constr: defining declarations on constr in Constr.Gravatar Hugo Herbelin2018-06-27
* Merge PR #7826: evd: restrict_evar with candidates, can raise NoCandidatesLeftGravatar Hugo Herbelin2018-06-26
|\
| * 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
* Update evarutil.mliGravatar Matthieu Sozeau2018-06-05
* Fix wrong deprecation msgGravatar Matthieu Sozeau2018-06-05
* [api] Remove deprecated objects in engine / interp / libraryGravatar Emilio Jesus Gallego Arias2018-05-30
* Split off Universes functions about substitutions and constraintsGravatar Gaëtan Gilbert2018-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
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* Merge PR #6935: Separate universe minimization and evar normalization functionsGravatar Pierre-Marie Pédrot2018-04-30
|\
* \ Merge PR #6866: Slight improvement of messages related to direct and indirect...Gravatar Pierre-Marie Pédrot2018-04-25
|\ \
| * | 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
|/ /
| * Deprecate mixing univ minimization and evm normalization functions.Gravatar Gaëtan Gilbert2018-04-17
|/
* Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
* Slightly refining some error messages about unresolvable evars.Gravatar Hugo Herbelin2018-03-24
* Cumulativity: improve treatment of irrelevant universes.Gravatar Gaëtan Gilbert2018-03-09
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Cleanup name-binding structure for fresh evar name generation.Gravatar Pierre-Marie Pédrot2018-01-02
* Merge PR #6222: Share computation of unifiable evarsGravatar Maxime Dénès2017-12-22
|\
* | [summary] Adapt STM to the new Summary API.Gravatar Emilio Jesus Gallego Arias2017-12-09
* | [api] Remove aliases of `Evar.t`Gravatar Emilio Jesus Gallego Arias2017-11-26
* | [api] A few more minor deprecation notices.Gravatar Emilio Jesus Gallego Arias2017-11-22
| * Experimenting with a fine-grained cache for undefined evars in evinfos.Gravatar Pierre-Marie Pédrot2017-11-21
|/
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Name.Id in core.Gravatar Emilio Jesus Gallego Arias2017-11-04
* Moving setting of "cleared" evar flag directly in Evd.restrict.Gravatar Hugo Herbelin2017-09-27
* Merge PR #830: Moving assert (the "Cut" rule) to new proof engineGravatar Maxime Dénès2017-08-29
|\
* | 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
|/
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Support for using type information to infer more precise evar sources.Gravatar Hugo Herbelin2017-05-30
* [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* Make the Constr.kind_of_term type parametric in sorts and universes.Gravatar Pierre-Marie Pédrot2017-03-31
* 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
* Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Removing some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
* Proofview.Goal primitive now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Rewrite API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Hints API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Leminv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Equality API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Refine API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-05 07:07:03 +0000