aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/miscops.ml
Commit message (Expand)AuthorAge
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Proper nametab handling of global universe namesGravatar Matthieu Sozeau2017-12-01
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * Allow flexible anonymous universes in instances and sorts.Gravatar Gaetan Gilbert2017-05-03
* | [location] Use located in misctypes.Gravatar Emilio Jesus Gallego Arias2017-04-24
|/
* Clenv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Univs: add Strict Universe Declaration option (on by default)Gravatar Matthieu Sozeau2015-10-07
* Fixing bug #4303: Anomaly: Uncaught exception Invalid_argument.Gravatar Pierre-Marie Pédrot2015-07-21
* Update headers.Gravatar Maxime Dénès2015-01-12
* Extend the syntax of simpl with a delta flag.Gravatar Arnaud Spiwack2014-12-12
* Avoid compilation warning.Gravatar Matthieu Sozeau2014-11-21
* Making map_union a standard function of the ML library.Gravatar Hugo Herbelin2014-11-19
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
* Seeing IntroWildcard as an action intro pattern rather than as a naming patternGravatar Hugo Herbelin2014-09-30
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
* Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codeGravatar Pierre Letouzey2014-03-02
* 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
* Updating headers.Gravatar herbelin2012-08-08
* 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