diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-09-15 17:31:51 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-08-01 17:54:42 +0200 |
| commit | a92b0e3abb476743f6f12ce828a0d82eb3c98e98 (patch) | |
| tree | 3a3284a60fff9ec15e876dba665969cd1bd24e27 /plugins/ltac/g_auto.ml4 | |
| parent | 533c4f693a557c81a13edc6e624ccaa9578c0ddc (diff) | |
Move type_uconstr to Tacinterp.
Diffstat (limited to 'plugins/ltac/g_auto.ml4')
| -rw-r--r-- | plugins/ltac/g_auto.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 301943a50..5baa0d5c1 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -48,7 +48,7 @@ let eval_uconstrs ist cs = expand_evars = true } in let map c env sigma = c env sigma in - List.map (fun c -> map (Pretyping.type_uconstr ~flags ist c)) cs + List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs let pr_auto_using_raw _ _ _ = Pptactic.pr_auto_using Ppconstr.pr_constr_expr let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> Printer.pr_glob_constr c) |