From fc2476e4a29592dcf2860a16d3a7c0aeeb4bffac Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 7 Nov 2014 18:38:12 +0100
Subject: Printing function for [uconstr].

The core is a "detyping" function for [closed_glob_constr]. Which interpretes the variable names according to the Ltac context, and apply the standard detyping procedure to typed terms in the closure.
---
 interp/constrextern.ml  | 8 ++++++++
 interp/constrextern.mli | 1 +
 2 files changed, 9 insertions(+)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 40e0901beb..fc40569624 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -959,6 +959,14 @@ let extern_type goal_concl_style env sigma t =
 
 let extern_sort s = extern_glob_sort (detype_sort s)
 
+let extern_closed_glob ?lax goal_concl_style env sigma t =
+  let avoid = if goal_concl_style then ids_of_context env else [] in
+  let r =
+    Detyping.detype_closed_glob ?lax goal_concl_style avoid env sigma t
+  in
+  let vars = vars_of_env env in
+  extern false (None,[]) vars r
+
 (******************************************************************)
 (* Main translation function from pattern -> constr_expr *)
 
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 804795480e..581ea4c5dc 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -28,6 +28,7 @@ val extern_glob_constr : Id.Set.t -> glob_constr -> constr_expr
 val extern_glob_type : Id.Set.t -> glob_constr -> constr_expr
 val extern_constr_pattern : names_context -> Evd.evar_map ->
   constr_pattern -> constr_expr
+val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob_constr -> constr_expr
 
 (** If [b=true] in [extern_constr b env c] then the variables in the first
    level of quantification clashing with the variables in [env] are renamed.
-- 
cgit v1.2.3