diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-08 09:54:42 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-05 08:58:20 +0100 |
| commit | 2e3ee15b03cf4b7428e1a7453385d79f434ec4a7 (patch) | |
| tree | fc399b19682aa528a73d90729c1e37ce4a761d6e /plugins/funind/recdef.ml | |
| parent | f22ad605a14eb14d11b0a1615f7014f2dca3b483 (diff) | |
Moving three related small half-general half-ad-hoc utility functions
next to each other, waiting for possible integration into a more
uniform API.
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index dd5381c76..6867939c2 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -29,6 +29,7 @@ open Proof_type open Pfedit open Glob_term open Pretyping +open Termops open Constrintern open Misctypes open Genredexpr |