diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 23:34:07 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-25 13:37:03 +0100 |
| commit | c4d62e3686926c27b172636ca8b746814d13a462 (patch) | |
| tree | c7a627b0fb392e187fe0cd72ed39656d56b81504 /ltac/g_auto.ml4 | |
| parent | a54579dd20e04ea919f8fa887e15dd82051fa297 (diff) | |
Moving type_uconstr to Pretyping.
Diffstat (limited to 'ltac/g_auto.ml4')
| -rw-r--r-- | ltac/g_auto.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4 index 788443944..bc98b7d6d 100644 --- a/ltac/g_auto.ml4 +++ b/ltac/g_auto.ml4 @@ -48,7 +48,7 @@ let eval_uconstrs ist cs = fail_evar = false; expand_evars = true } in - List.map (fun c -> Tacinterp.type_uconstr ~flags ist c) cs + List.map (fun c -> Pretyping.type_uconstr ~flags ist c) cs let pr_auto_using _ _ _ = Pptactic.pr_auto_using (fun _ -> mt ()) |