From a92b0e3abb476743f6f12ce828a0d82eb3c98e98 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Sep 2016 17:31:51 +0200
Subject: Move type_uconstr to Tacinterp.

---
 plugins/ltac/tacinterp.ml | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'plugins/ltac/tacinterp.ml')

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index d3e625e73a..51eed2f4ec 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 () ->
-- 
cgit v1.2.3