aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/indfun.mli
Commit message (Expand)AuthorAge
* [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* [ssreflect] Fix module scoping problems due to packing and mli files.Gravatar Emilio Jesus Gallego Arias2018-03-10
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
* Removing Proof_type from the API.Gravatar Pierre-Marie Pédrot2017-06-16
* Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* Funind API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* Lazy interpretation of patterns so that expressions such as "intros H H'/H"Gravatar Hugo Herbelin2014-08-18
* 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
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Using vernac parsing for FunctionGravatar jforest2010-06-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-13 17:07:02 +0000