From e4db6e726b5307c35e99a02cacbd96290e80dd24 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 6 Sep 2017 14:11:00 +0200
Subject: Code factorization.

---
 src/tac2core.ml   | 7 +------
 src/tac2quote.mli | 2 ++
 2 files changed, 3 insertions(+), 6 deletions(-)

(limited to 'src')

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
-- 
cgit v1.2.3