diff options
| author | Pierre-Marie Pédrot | 2017-09-06 14:11:00 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-06 14:11:00 +0200 |
| commit | e4db6e726b5307c35e99a02cacbd96290e80dd24 (patch) | |
| tree | 497c80f8a3f364bf1ad8b3ca137bd1ff996782d4 | |
| parent | 217bd80b651d2d12b05f74cf21485eb0fea8e3e3 (diff) | |
Code factorization.
| -rw-r--r-- | src/tac2core.ml | 7 | ||||
| -rw-r--r-- | src/tac2quote.mli | 2 |
2 files changed, 3 insertions, 6 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index cd39cb6f27..2c9226adae 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -1012,11 +1012,6 @@ let scope_fail s args = let q_unit = Loc.tag @@ CTacCst (AbsKn (Tuple 0)) -let rthunk e = - let loc = Tac2intern.loc_of_tacexpr e in - let var = [Loc.tag ?loc @@ CPatVar Anonymous, Some (Loc.tag ?loc @@ CTypRef (AbsKn (Other Core.t_unit), []))] in - Loc.tag ?loc @@ CTacFun (var, e) - let add_generic_scope s entry arg = let parse = function | [] -> @@ -1118,7 +1113,7 @@ end let () = add_scope "thunk" begin function | [tok] -> let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in - let act e = rthunk (act e) in + let act e = Tac2quote.thunk (act e) in Tac2entries.ScopeRule (scope, act) | arg -> scope_fail "thunk" arg end diff --git a/src/tac2quote.mli b/src/tac2quote.mli index db2fda3831..9f42c60042 100644 --- a/src/tac2quote.mli +++ b/src/tac2quote.mli @@ -20,6 +20,8 @@ open Tac2expr val constructor : ?loc:Loc.t -> ltac_constructor -> raw_tacexpr list -> raw_tacexpr +val thunk : raw_tacexpr -> raw_tacexpr + val of_anti : ('a -> raw_tacexpr) -> 'a or_anti -> raw_tacexpr val of_int : int located -> raw_tacexpr |