Some dead code removal, thanks to Oug analyzer

 In particular, the unused lib/tlm.ml and lib/gset.ml are removed

 In addition, to simplify code, Libobject.record_object returning only the
 ('a->obj) function, which is enough almost all the time.
 Use Libobject.record_object_full if you really need also the (obj->'a).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 25 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 3f899a8ec1..4ad823e066 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1394,33 +1394,8 @@ let check_evars env initial_sigma sigma c =
       | _ -> iter_constr proc_rec c
   in proc_rec c
 
-(* Substitutes undefined evars by evars of same context up to renaming *)
-
-let subst_evar_evar subst c =
-  let rec aux c = match kind_of_term c with
-  | Evar (evk,args) ->
-      let evk' = try ExistentialMap.find evk subst with Not_found -> evk in
-      mkEvar (evk',Array.map aux args)
-  | _ -> map_constr aux c
-  in aux c
-
-let subst_undefined_evar_info_evar subst evi =
-  { evi with
-    evar_hyps = map_named_val (subst_evar_evar subst) evi.evar_hyps;
-    evar_concl = subst_evar_evar subst evi.evar_concl }
-
 open Rawterm
 
-let subst_evar_evar_in_constr_with_bindings subst (c,bl) =
-  (subst_evar_evar subst c,
-   match bl with
-   | ImplicitBindings largs ->
-       ImplicitBindings (List.map (subst_evar_evar subst) largs)
-   | ExplicitBindings lbind ->
-       ExplicitBindings (List.map (on_pi3 (subst_evar_evar subst)) lbind)
-   | NoBindings ->
-       NoBindings)
-
 (* Operations on value/type constraints *)
 
 type type_constraint_type = (int * int) option * constr