diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-11-07 14:47:15 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-11-07 14:47:15 +0100 |
| commit | 1f36cdefd841526f804bd2dd51c1d88309333376 (patch) | |
| tree | 9d13ea499cfebf6285eccc6d8b434bcf5ea9e41b /tactics/hints.ml | |
| parent | a4cecc13cde3239d6a86f98ba6bba0e4554306bd (diff) | |
Fixes to compile with ocaml 4.01
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 9cbfe20d9..53573bc7e 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -84,7 +84,9 @@ let secvars_of_hyps hyps = if all then Id.Pred.full (* If the whole section context is available *) else pred -let empty_hint_info = Vernacexpr.{ hint_priority = None; hint_pattern = None } +let empty_hint_info = + let open Vernacexpr in + { hint_priority = None; hint_pattern = None } (************************************************************************) (* The Type of Constructions Autotactic Hints *) |