aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/g_indfun.ml4
Commit message (Expand)AuthorAge
* Remove reference name type.Gravatar Maxime Dénès2018-06-18
* [api] Misctypes removal: move Tactypes to proofsGravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* Merge PR #7558: [api] Make `vernac/` self-contained.Gravatar Maxime Dénès2018-05-30
|\
| * [api] Make `vernac/` self-contained.Gravatar Emilio Jesus Gallego Arias2018-05-27
* | Remove some occurrences of Evd.emptyGravatar Maxime Dénès2018-05-25
|/
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
* [vernac] vernac_expr no longer recursiveGravatar Vincent Laporte2018-01-08
* Separate vernac controls and regular commands.Gravatar Maxime Dénès2017-12-20
* Remove "obsolete_locality" and fix STM vernac classification.Gravatar Maxime Dénès2017-11-29
* Using a specific function to register vernac printers.Gravatar Hugo Herbelin2017-11-02
* Parse directly to Sorts.family when appropriate.Gravatar Gaëtan Gilbert2017-09-08
* [api] Remove type equalities from API.Gravatar Emilio Jesus Gallego Arias2017-07-25
* [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* [printing] Remove duplicated printing function.Gravatar Emilio Jesus Gallego Arias2017-06-01
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Use located in misctypes.Gravatar Emilio Jesus Gallego Arias2017-04-24
|/
* Merge PR#379: Introducing evar-insensitive constrsGravatar Maxime Dénès2017-04-11
|\
* | [camlpX] Remove camlp4 compat layer.Gravatar Emilio Jesus Gallego Arias2017-04-07
| * Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
| |\ | |/ |/|
* | Moving the Ltac plugin to a pack-based one.Gravatar Pierre-Marie Pédrot2017-02-17
| * Funind API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| * Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| * Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|/
* Merging Stdarg and Constrarg.Gravatar Pierre-Marie Pédrot2016-09-21
* Moving Ltac-specific parsing API to ltac/ folder.Gravatar Pierre-Marie Pédrot2016-09-14
* rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...Gravatar Pierre Letouzey2016-07-03
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* Fixing a mispelling coma -> comma.Gravatar Hugo Herbelin2016-06-16
* Fixing printing of Function.Gravatar Hugo Herbelin2016-06-16
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* More toplevel value representation sharing.Gravatar Pierre-Marie Pédrot2016-05-04
* Revert "Fixing printing of Function."Gravatar Hugo Herbelin2016-04-27
* Revert "Fixing a mispelling coma -> comma."Gravatar Hugo Herbelin2016-04-27
* Fixing a mispelling coma -> comma.Gravatar Hugo Herbelin2016-04-27
* Fixing printing of Function.Gravatar Hugo Herbelin2016-04-27
* Removing the special status of generic arguments defined by Coq itself.Gravatar Pierre-Marie Pédrot2016-03-17
* Removing the special status of generic entries defined by Coq itself.Gravatar Pierre-Marie Pédrot2016-03-17
* Adding a universe argument to Pcoq.create_generic_entry.Gravatar Pierre-Marie Pédrot2016-03-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-13 14:29:11 +0000