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/tacinterp.ml | |
| parent | a54579dd20e04ea919f8fa887e15dd82051fa297 (diff) | |
Moving type_uconstr to Pretyping.
Diffstat (limited to 'ltac/tacinterp.ml')
| -rw-r--r-- | ltac/tacinterp.ml | 18 |
1 files changed, 0 insertions, 18 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 4506f8159..4c74984f8 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -723,24 +723,6 @@ let interp_open_constr_list = let pf_interp_type ist env sigma = interp_type ist env sigma -(* Fully evaluate an untyped constr *) -let type_uconstr ?(flags = constr_flags) - ?(expected_type = WithoutTypeConstraint) ist c = - { delayed = begin fun env sigma -> - let open Pretyping in - let { closure; term } = c in - let vars = { - ltac_constrs = closure.typed; - ltac_uconstrs = closure.untyped; - ltac_idents = closure.idents; - ltac_genargs = ist.lfun; - } in - let sigma = Sigma.to_evar_map sigma in - let (sigma, c) = understand_ltac flags env sigma vars expected_type term in - Sigma.Unsafe.of_pair (c, sigma) - end } - - (* Interprets a reduction expression *) let interp_unfold ist env sigma (occs,qid) = (interp_occurrences ist occs,interp_evaluable ist env sigma qid) |