aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/miscops.ml
Commit message (Expand)AuthorAge
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-02 16:41:43 +0000