aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/glob_term.ml
Commit message (Expand)AuthorAge
* Remove reference name type.Gravatar Maxime Dénès2018-06-18
* [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Move universe syntax to `Glob_term`Gravatar Emilio Jesus Gallego Arias2018-05-08
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* [api] Relocate `intf` modules according to dependency-order.Gravatar Emilio Jesus Gallego Arias2018-04-23
* Glob_term now mli-only, operations now in Glob_opsGravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Evar_kinds.mli containing former Evd.hole_kind, avoid deps on EvdGravatar letouzey2012-05-29
* Glob_term.predicate_pattern: No number of parameters with letins.Gravatar pboutill2012-03-02
* Noise for nothingGravatar pboutill2012-03-02
* Added an pattern / occurence syntax for vm_compute.Gravatar ppedrot2012-01-30
* Remove dynamic stuff from constr_expr and glob_constrGravatar glondu2011-10-28
* Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".Gravatar herbelin2011-04-15
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 16:10:01 +0000