diff options
| author | Yves Bertot | 2018-11-07 14:04:06 +0100 |
|---|---|---|
| committer | GitHub | 2018-11-07 14:04:06 +0100 |
| commit | e6f4d7f40b4764b3ef7c9e996003b5e614d3ae2e (patch) | |
| tree | f8ca5d6e658e20660ff973a98574e83f9e90f427 | |
| parent | f8b340ee5d1adce859f5b394c736f7cd60e0b9fb (diff) | |
| parent | 6cc40e73879aec50227c9576100a381cc11ade30 (diff) | |
Merge pull request #17 from ejgallego/fix_warn
[warnings] Fix couple of warnings related to API..
| -rw-r--r-- | tuto1/src/simple_declare.ml | 8 | ||||
| -rw-r--r-- | tuto3/src/tuto_tactic.ml | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml index af4dd5bddf..50fd170663 100644 --- a/tuto1/src/simple_declare.ml +++ b/tuto1/src/simple_declare.ml @@ -1,10 +1,10 @@ +(* Ideally coq/coq#8811 would get merged and then this function could be much simpler. *) let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook = - let open EConstr in let sigma = Evd.minimize_universes sigma in - let body = to_constr sigma body in - let tyopt = Option.map (to_constr sigma) tyopt in + let body = EConstr.to_constr sigma body in + let tyopt = Option.map (EConstr.to_constr sigma) tyopt in let uvars_fold uvars c = - Univ.LSet.union uvars (Univops.universes_of_constr c) in + Univ.LSet.union uvars (Vars.universes_of_constr c) in let uvars = List.fold_left uvars_fold Univ.LSet.empty (Option.List.cons tyopt [body]) in let sigma = Evd.restrict_universe_context sigma uvars in diff --git a/tuto3/src/tuto_tactic.ml b/tuto3/src/tuto_tactic.ml index cb73a4486b..9818867621 100644 --- a/tuto3/src/tuto_tactic.ml +++ b/tuto3/src/tuto_tactic.ml @@ -15,7 +15,7 @@ let collect_constants () = let gr_R = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "pair" in let gr_P = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "prod" in let gr_U = find_reference "Tuto3" ["Tuto3"; "Data"] "uncover" in - constants := List.map (fun x -> of_constr (constr_of_global x)) + constants := List.map (fun x -> of_constr (constr_of_monomorphic_global x)) [gr_H; gr_M; gr_R; gr_P; gr_U]; !constants else |