Remove some unused functions.

Note: they do not even seem to have a debugging purpose, so better remove
them before they bitrot.

3 files changed, 0 insertions, 35 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index fe26dcd28..69e8e9d98 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1007,21 +1007,6 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs =
  * Note: argument f is the function used to instantiate evars.
  *)
 
-let are_canonical_instances args1 args2 env =
-  let n1 = Array.length args1 in
-  let n2 = Array.length args2 in
-  let rec aux n = function
-    | (id,_,c)::sign
-        when n < n1 && isVarId id args1.(n) && isVarId id args2.(n) ->
-        aux (n+1) sign
-    | [] ->
-        let rec aux2 n =
-          Int.equal n n1 ||
-          (isRelN (n1-n) args1.(n) && isRelN (n1-n) args2.(n) && aux2 (n+1))
-        in aux2 n
-    | _ -> false in
-  Int.equal n1 n2 && aux 0 (named_context env)
-
 let filter_compatible_candidates conv_algo env evd evi args rhs c =
   let c' = instantiate_evar_array evi c args in
   match conv_algo env evd Reduction.CONV rhs c' with
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f5b89e789..7d5496917 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -444,26 +444,12 @@ let new_type_evar env evdref loc =
       univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)) evdref
   in e
 
-let get_projection env cst =
-  let cb = lookup_constant cst env in
-    match cb.Declarations.const_proj with
-    | Some {Declarations.proj_ind = mind; proj_npars = n;
-	    proj_arg = m; proj_type = ty} -> 
-      (cst,mind,n,m,ty)
-    | None -> raise Not_found
-
 let (f_genarg_interp, genarg_interp_hook) = Hook.make ()
 
 (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
 (* in environment [env], with existential variables [evdref] and *)
 (* the type constraint tycon *)
 
-let is_GHole = function
-  | GHole _ -> true
-  | _ -> false
-
-let evars = ref Id.Map.empty
-
 let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t =
   let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in
   let pretype_type = pretype_type k0 resolve_tc in
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 48911a5a9..31e75e550 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -940,8 +940,6 @@ let matches_head env sigma c t =
     | Proj (p, _) -> Constr_matching.matches env sigma c (mkConst (Projection.constant p))
     | _ -> raise Constr_matching.PatternMatchingFailure
 
-let is_pattern_meta = function Pattern.PMeta _ -> true | _ -> false
-
 (** FIXME: Specific function to handle projections: it ignores what happens on the
     parameters. This is a temporary fix while rewrite etc... are not up to equivalence
     of the projection and its eta expanded form.
@@ -1055,10 +1053,6 @@ let unfold env sigma name =
   else
     error (string_of_evaluable_ref env name^" is opaque.")
 
-let is_projection env = function
-  | EvalVarRef _ -> false
-  | EvalConstRef c -> Environ.is_projection c env
-
 (* [unfoldoccs : (readable_constraints -> (int list * full_path) -> constr -> constr)]
  * Unfolds the constant name in a term c following a list of occurrences occl.
  * at the occurrences of occ_list. If occ_list is empty, unfold all occurrences.