diff options
Diffstat (limited to 'kernel/mod_subst.ml')
| -rw-r--r-- | kernel/mod_subst.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 009bcb770..f0d1aca4d 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -546,6 +546,9 @@ let force fsubst r = match r.subst_subst with let subst_substituted s r = { r with subst_subst = s :: r.subst_subst; } +let force_constr = force subst_mps +let subst_constr = subst_substituted + (* debug *) let repr_substituted r = match r.subst_subst with | [] -> None, r.subst_value |