diff options
| -rw-r--r-- | proofs/clenv.ml | 2 | ||||
| -rw-r--r-- | proofs/clenv.mli | 2 |
2 files changed, 4 insertions, 0 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index eb91ade44a..f59226e893 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -216,6 +216,7 @@ let subst_clenv f sub clenv = let connect_clenv wc clenv = { clenv with hook = wc } +(* Was used in wcclausenv.ml (* Changes the head of a clenv with (templ,templty) *) let clenv_change_head (templ,templty) clenv = { templval = mk_freelisted templ; @@ -223,6 +224,7 @@ let clenv_change_head (templ,templty) clenv = namenv = clenv.namenv; env = clenv.env; hook = clenv.hook } +*) let mk_clenv_hnf_constr_type_of wc t = mk_clenv_from wc (t,w_hnf_constr wc (w_type_of wc t)) diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 3babd9224e..0ccdf450e9 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -69,7 +69,9 @@ val subst_clenv : (substitution -> 'a -> 'a) -> substitution -> 'a clausenv -> 'a clausenv val connect_clenv : wc -> 'a clausenv -> wc clausenv +(*i Was used in wcclausenv.ml val clenv_change_head : constr * constr -> 'a clausenv -> 'a clausenv +i*) val clenv_assign : metavariable -> constr -> 'a clausenv -> 'a clausenv val clenv_instance_term : wc clausenv -> constr -> constr val clenv_pose : name * metavariable * constr -> 'a clausenv -> 'a clausenv |