diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-02-24 20:46:32 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-02-26 14:53:08 +0100 |
| commit | 15b6c9b6fa268a9af6dd4f05961e469545e92a6f (patch) | |
| tree | 2e5aacf72993b448d1e80b0cbfbf0a09091ecb32 /kernel/mod_subst.ml | |
| parent | e6556db92d4c4fe9ba38f26b89f805095d2b2638 (diff) | |
Lazyconstr -> Opaqueproof
Make this module deal only with opaque proofs.
Make discharging/substitution invariant more explicit via a third constructor.
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 |