diff options
| author | herbelin | 2003-10-10 18:51:54 +0000 |
|---|---|---|
| committer | herbelin | 2003-10-10 18:51:54 +0000 |
| commit | 80ec30c8ee117631ff5422bb158e38d847935258 (patch) | |
| tree | 659447af46da45aca32320da5e2c4dea5443b78c | |
| parent | af5a0cccac41237723d118027a71d00b6ec5218e (diff) | |
Suppression clenv_change_head que seul Wcclausenv utisait
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4572 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |