diff options
| author | Arnaud Spiwack | 2014-08-01 19:14:27 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-08-01 19:18:59 +0200 |
| commit | 94b201b0a7b03978d96b8f8c9d631e4fa4bda4b0 (patch) | |
| tree | 998601ebfb4ad8163bd6c3fb81fabe331c154947 /tactics | |
| parent | b240b7d0cfd6233dcb0ba0e3b98354c78c23a0d4 (diff) | |
Faster uconstr.
Detyping was called on every typed constr in the Ltac context which was costly as most of the context is likely not to be refered to in a particular uconstr. This commit calls detyping lazily instead.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/taccoerce.ml | 4 | ||||
| -rw-r--r-- | tactics/taccoerce.mli | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml index 4152218197..0697ae5529 100644 --- a/tactics/taccoerce.ml +++ b/tactics/taccoerce.ml @@ -150,10 +150,10 @@ let coerce_to_constr env v = let coerce_to_uconstr env v = let v = Value.normalize v in if has_type v (topwit wit_uconstr) then - out_gen (topwit wit_uconstr) v + Lazy.lazy_from_val (out_gen (topwit wit_uconstr) v) else let (_ctx,c) = coerce_to_constr env v in - Detyping.detype false [] [] c + lazy (Detyping.detype false [] [] c) let coerce_to_closed_constr env v = let ids,c = coerce_to_constr env v in diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli index b4c0283c92..171269f929 100644 --- a/tactics/taccoerce.mli +++ b/tactics/taccoerce.mli @@ -58,7 +58,7 @@ val coerce_to_int : Value.t -> int val coerce_to_constr : Environ.env -> Value.t -> constr_under_binders -val coerce_to_uconstr : Environ.env -> Value.t -> Glob_term.glob_constr +val coerce_to_uconstr : Environ.env -> Value.t -> Glob_term.glob_constr Lazy.t val coerce_to_closed_constr : Environ.env -> Value.t -> constr |