aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/indfun.mli
Commit message (Expand)AuthorAge
* 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-12-04 09:39:20 +0000