diff options
| author | Emilio Jesus Gallego Arias | 2018-02-14 02:05:42 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-03-01 01:44:12 +0100 |
| commit | 5cb74f82165e88c5e527ad757b007df1fbe5f1b3 (patch) | |
| tree | 9982edb4e98ffb4b178f2e55d2fcbe7da4903c8c /src | |
| parent | 880e87269073de20d57e0d309bbc9b343f8444d5 (diff) | |
[api] Remove some deprecation warnings.
Trivial commit.
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2core.ml | 4 | ||||
| -rw-r--r-- | src/tac2ffi.mli | 2 | ||||
| -rw-r--r-- | src/tac2quote.ml | 2 |
3 files changed, 5 insertions, 3 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index 1afaea8bd9..c16e72b801 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -894,7 +894,9 @@ let () = let () = let intern self ist c = - let _, pat = Constrintern.intern_constr_pattern ist.Genintern.genv ~as_type:false c in + let env = ist.Genintern.genv in + let sigma = Evd.from_env env in + let _, pat = Constrintern.intern_constr_pattern env sigma ~as_type:false c in GlbVal pat, gtypref t_pattern in let print env pat = str "pattern:(" ++ Printer.pr_lconstr_pattern_env env Evd.empty pat ++ str ")" in diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli index 4d77c989f3..1bf86b516a 100644 --- a/src/tac2ffi.mli +++ b/src/tac2ffi.mli @@ -165,7 +165,7 @@ val val_constant : Constant.t Val.tag val val_constructor : constructor Val.tag val val_projection : Projection.t Val.tag val val_case : Constr.case_info Val.tag -val val_univ : Univ.universe_level Val.tag +val val_univ : Univ.Level.t Val.tag val val_free : Id.Set.t Val.tag val val_exn : Exninfo.iexn Tac2dyn.Val.tag diff --git a/src/tac2quote.ml b/src/tac2quote.ml index d0c1365eff..829f13344c 100644 --- a/src/tac2quote.ml +++ b/src/tac2quote.ml @@ -221,7 +221,7 @@ let pattern_vars pat = let () = check_pattern_id ?loc:pat.CAst.loc id in Id.Set.add id accu | _ -> - Topconstr.fold_constr_expr_with_binders (fun _ () -> ()) aux () accu pat + Constrexpr_ops.fold_constr_expr_with_binders (fun _ () -> ()) aux () accu pat in aux () Id.Set.empty pat |