[uconstr]: use a closure instead of eager substitution.

This avoids relying on detyping. As Matthieu Sozeau pointed out to me, [understand∘detyping] has no reason to be the identity. This may create surprising behaviour some times (when a detyped term loses its relations to the current context, in particular in terms of universes), and downright incompatibilities in the case of refine.

As a bonus this should be a faster implementation of [uconstr] with a leaner memory profile.

1 files changed, 10 insertions, 0 deletions

diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index d379552254..ec27aab338 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -72,3 +72,13 @@ and cases_clause = (Loc.t * Id.t list * cases_pattern list * glob_constr)
 (** [(p,il,cl,t)] = "|'cl' => 't'". Precondition: the free variables
     of [t] are members of [il]. *)
 and cases_clauses = cases_clause list
+
+(** A globalised term together with a closure representing the value
+    of its free variables. Intended for use when these variables are taken
+    from the Ltac environment. *)
+type closure = {
+  typed: Pattern.constr_under_binders Id.Map.t ;
+  untyped:closed_glob_constr Id.Map.t }
+and closed_glob_constr = {
+  closure: closure;
+  term: glob_constr }