Slightly more compact representation of 'a substituted type,

removing an unneeded indirection.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16781 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 4 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index 7e0cae20a..93dc84fa5 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -128,11 +128,12 @@ type substitution = (module_path * delta_resolver) umap_t
 
 (** {6 Delayed constr} *)
 
-type 'a lazy_subst =
-  | LSval of 'a
-  | LSlazy of substitution list * 'a
+type 'a substituted = {
+  mutable subst_value : 'a;
+  mutable subst_subst : substitution list;
+}
 
-type constr_substituted = constr lazy_subst ref
+type constr_substituted = constr substituted
 
 (** Nota : in coqtop, the [lazy_constr] type also have a [Direct]
     constructor, but it shouldn't occur inside a .vo, so we ignore it *)