diff options
| author | Yves Bertot | 2018-10-01 13:43:36 +0200 |
|---|---|---|
| committer | Yves Bertot | 2018-10-01 13:43:36 +0200 |
| commit | ed3e5e036ee72f40ffca92775339dcc227d58f79 (patch) | |
| tree | 9db30e2bf0d02a63b3adb5d570e247320261c2f2 /tuto3 | |
| parent | b303b75c18734accc9cd7efe82307b0424426e3f (diff) | |
adapts to master on Oct. 1st 2018, but warnings remain
Diffstat (limited to 'tuto3')
| -rw-r--r-- | tuto3/src/tuto_tactic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tuto3/src/tuto_tactic.ml b/tuto3/src/tuto_tactic.ml index fbb6863f7e..3e926ad7f2 100644 --- a/tuto3/src/tuto_tactic.ml +++ b/tuto3/src/tuto_tactic.ml @@ -9,7 +9,7 @@ let collect_constants () = if (!constants = []) then let open Coqlib in let open EConstr in - let open Universes in + let open UnivGen 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 |