diff options
| author | Gaëtan Gilbert | 2019-01-07 14:09:58 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-08 16:41:11 +0100 |
| commit | 8801a2304d54e687dafc8614af38f69ada2cbee1 (patch) | |
| tree | 46276fc288a7f9a6320da58fbe52a4989fb17e06 /doc/plugin_tutorial/tuto3/src/tuto_tactic.ml | |
| parent | 748d1d957b4f866cdb10671f4383be05a1105d06 (diff) | |
plugin_tutorial: ignore Coqlib.find_reference deprecation warning.
Not sure what the right solution is here, but we can improve after the merge.
Diffstat (limited to 'doc/plugin_tutorial/tuto3/src/tuto_tactic.ml')
| -rw-r--r-- | doc/plugin_tutorial/tuto3/src/tuto_tactic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml index 9818867621..8f2c387d09 100644 --- a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml +++ b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml @@ -7,9 +7,9 @@ let constants = ref ([] : EConstr.t list) c_U *) let collect_constants () = if (!constants = []) then - let open Coqlib in let open EConstr in let open UnivGen in + let find_reference = Coqlib.find_reference [@ocaml.warning "-3"] in let gr_H = find_reference "Tuto3" ["Tuto3"; "Data"] "pack" in let gr_M = find_reference "Tuto3" ["Tuto3"; "Data"] "packer" in let gr_R = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "pair" in |