diff options
| author | Maxime Dénès | 2017-04-07 19:22:55 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-07 19:24:17 +0200 |
| commit | 197a45551c133b5b386188bdf1d6a3739a6a3561 (patch) | |
| tree | c7bd1982c38906e34462fe4fd33d7806de9c52c6 /plugins/funind | |
| parent | 3fb4d9dfc270aa7d4ea09fabbf857cfc11607019 (diff) | |
| parent | 2d6ebc9d8bffd5910f201af75a0b3e45dd9c8988 (diff) | |
Merge PR#461: [camlpX] Remove camlp4 compat layer.
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 368b23be30..cf2e42d2c9 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -7,7 +7,6 @@ (************************************************************************) (*i camlp4deps: "grammar/grammar.cma" i*) open Ltac_plugin -open Compat open Util open Term open Pp @@ -17,6 +16,7 @@ open Indfun open Genarg open Stdarg open Misctypes +open Pcoq open Pcoq.Prim open Pcoq.Constr open Pltac |