From 80ec30c8ee117631ff5422bb158e38d847935258 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 10 Oct 2003 18:51:54 +0000
Subject: 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
---
 proofs/clenv.ml  | 2 ++
 proofs/clenv.mli | 2 ++
 2 files changed, 4 insertions(+)

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
-- 
cgit v1.2.3