aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/misctypes.mli
Commit message (Expand)AuthorAge
* Allow flexible anonymous universes in instances and sorts.Gravatar Gaetan Gilbert2017-05-03
* Attempt to improve error message when "apply in" fail.Gravatar Hugo Herbelin2017-03-15
* Untangling Tacexpr from lower strata.Gravatar Pierre-Marie Pédrot2016-09-15
* Unplugging Tacexpr in several interface files.Gravatar Pierre-Marie Pédrot2016-09-08
* New step on recent 9c2662eecc398f3 (strong invariants on tuple pattern).Gravatar Hugo Herbelin2016-01-21
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
* | Stronger invariants on the use of the introduction pattern (pat1,...,patn).Gravatar Hugo Herbelin2016-01-21
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | COMMENTS: added to some variants of "Misctypes.glob_sort_gen" type.Gravatar Matej Kosik2015-12-18
|/
* Univs: add Strict Universe Declaration option (on by default)Gravatar Matthieu Sozeau2015-10-07
* Update headers.Gravatar Maxime Dénès2015-01-12
* Seeing IntroWildcard as an action intro pattern rather than as a naming patternGravatar Hugo Herbelin2014-09-30
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
* Reorganisation of intropattern codeGravatar Hugo Herbelin2014-08-18
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* Declaremods: major refactoring, stop duplicating libobjects in modulesGravatar letouzey2013-07-17
* Revising r16550 about providing intro patterns for applying injection:Gravatar herbelin2013-07-09
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Modulification of identifierGravatar ppedrot2012-12-14
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* avoid referring to Term in constrexpr.mli and glob_term.mliGravatar letouzey2012-10-02
* Updating headers.Gravatar herbelin2012-08-08
* Avoid Pp.std_ppcmds in Misctypes.sort_infoGravatar letouzey2012-08-07
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* No more Univ in grammar.cmaGravatar letouzey2012-05-29
* 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