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/tacinterp.ml | |
| parent | 533c4f693a557c81a13edc6e624ccaa9578c0ddc (diff) | |
Move type_uconstr to Tacinterp.
Diffstat (limited to 'plugins/ltac/tacinterp.ml')
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index d3e625e73..51eed2f4e 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1108,6 +1108,20 @@ let rec read_match_rule lfun ist env sigma = function :: read_match_rule lfun ist env sigma tl | [] -> [] +(* Fully evaluate an untyped constr *) +let type_uconstr ?(flags = {(constr_flags ()) with use_hook = None }) + ?(expected_type = WithoutTypeConstraint) ist c = + begin fun env sigma -> + let { closure; term } = c in + let vars = { + ltac_constrs = closure.typed; + ltac_uconstrs = closure.untyped; + ltac_idents = closure.idents; + ltac_genargs = Id.Map.empty; + } in + understand_ltac flags env sigma vars expected_type term + end + let warn_deprecated_info = CWarnings.create ~name:"deprecated-info-tactical" ~category:"deprecated" (fun () -> |