Removing dead code, thanks to new OCaml warnings and a bit of scripting.

10 files changed, 0 insertions, 60 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 444043dbe..64a9f0024 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -23,7 +23,6 @@ open Tacred
 open Pretype_errors
 open Evarutil
 open Unification
-open Mod_subst
 open Misctypes
 
 (* Abbreviations *)
@@ -43,12 +42,6 @@ type clausenv = {
 let cl_env ce = ce.env
 let cl_sigma ce =  ce.evd
 
-let subst_clenv sub clenv =
-  { templval = map_fl (subst_mps sub) clenv.templval;
-    templtyp = map_fl (subst_mps sub) clenv.templtyp;
-    evd = subst_evar_defs_light sub clenv.evd;
-    env = clenv.env }
-
 let clenv_nf_meta clenv c = nf_meta clenv.evd c
 let clenv_term clenv c = meta_instance clenv.evd c
 let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv
@@ -304,8 +297,6 @@ let clenv_pose_metas_as_evars clenv dep_mvs =
 	fold clenv mvs in
   fold clenv dep_mvs
 
-let evar_clenv_unique_resolver = clenv_unique_resolver
-
 (******************************************************************)
 
 let connect_clenv gls clenv =
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index e74c4875f..ab4f3af79 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -23,11 +23,6 @@ type clausenv = {
 				    out *)
   templtyp : constr freelisted (** its type *)}
 
-(** Substitution is not applied on templenv (because [subst_clenv] is
-   applied only on hints which typing env is overwritten by the
-   goal env) *)
-val subst_clenv : substitution -> clausenv -> clausenv
-
 (** subject of clenv (instantiated) *)
 val clenv_value     : clausenv -> constr
 
@@ -62,11 +57,6 @@ val clenv_unify :
 val clenv_unique_resolver :
   ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
 
-(** same as above ([allow_K=false]) but replaces remaining metas
-   with fresh evars if [evars_flag] is [true] *)
-val evar_clenv_unique_resolver :
-  ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
-
 val clenv_dependent : clausenv -> metavariable list
 
 val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index c0036d192..7a1a14bde 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -79,9 +79,6 @@ let dft = default_unify_flags
 let res_pf clenv ?(with_evars=false) ?(flags=dft) gls =
   clenv_refine with_evars (clenv_unique_resolver ~flags clenv gls) gls
 
-let e_res_pf clenv = res_pf clenv ~with_evars:true ~flags:dft
-
-
 (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
    particulier ne semblent pas vérifier que des instances différentes
    d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index f635012fe..173eb32e3 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -19,6 +19,3 @@ val res_pf : clausenv -> ?with_evars:evars_flag -> ?flags:unify_flags -> tactic
 
 val clenv_pose_dependent_evars : evars_flag -> clausenv -> clausenv
 val clenv_value_cast_meta : clausenv -> constr
-
-(** Compatibility, use res_pf ?with_evars:true instead *)
-val e_res_pf : clausenv -> tactic
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 30905e577..054e6db6c 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -695,12 +695,6 @@ let prim_refiner r sigma goal =
 	let sigma = Goal.V82.partial_solution sigma goal ev in
   	  ([gl], sigma)
 
-    | Order ord ->
-        let hyps' = reorder_val_context env sign ord in
-	let (gl,ev,sigma) = mk_goal hyps' cl in
-	let sigma = Goal.V82.partial_solution sigma goal ev in
-        ([gl], sigma)
-
     | Rename (id1,id2) ->
         if !check && not (Id.equal id1 id2) &&
 	  Id.List.mem id2
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index f98bfa5ea..7297706e1 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -37,7 +37,6 @@ type prim_rule =
   | Thin of Id.t list
   | ThinBody of Id.t list
   | Move of bool * Id.t * Id.t move_location
-  | Order of Id.t list
   | Rename of Id.t * Id.t
 
 (** Nowadays, the only rules we'll consider are the primitive rules *)
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index a5d694077..0aadd862b 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -29,7 +29,6 @@ type prim_rule =
   | Thin of Id.t list
   | ThinBody of Id.t list
   | Move of bool * Id.t * Id.t move_location
-  | Order of Id.t list
   | Rename of Id.t * Id.t
 
 (** Nowadays, the only rules we'll consider are the primitive rules *)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 2ea877725..f73bdaf93 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -65,10 +65,6 @@ val tclTHENSV         : tactic -> tactic array -> tactic
 (** Same with a list of tactics *)
 val tclTHENS         : tactic -> tactic list -> tactic
 
-(** [tclTHENST] is renamed [tclTHENSFIRSTn]
-val tclTHENST        : tactic -> tactic array -> tactic -> tactic
-*)
-
 (** [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
    applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to
    the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m]
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 0f898feef..a36b7f2ac 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -71,8 +71,6 @@ let pf_get_new_ids ids gls =
 
 let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id
 
-let pf_parse_const gls = compose (pf_global gls) Id.of_string
-
 let pf_reduction_of_red_expr gls re c =
   (fst (reduction_of_red_expr (pf_env gls) re)) (pf_env gls) (project gls) c
 
@@ -80,9 +78,7 @@ let pf_apply f gls = f (pf_env gls) (project gls)
 let pf_reduce = pf_apply
 
 let pf_whd_betadeltaiota         = pf_reduce whd_betadeltaiota
-let pf_whd_betadeltaiota_stack   = pf_reduce whd_betadeltaiota_stack
 let pf_hnf_constr                = pf_reduce hnf_constr
-let pf_red_product               = pf_reduce red_product
 let pf_nf                        = pf_reduce simpl
 let pf_nf_betaiota               = pf_reduce (fun _ -> nf_betaiota)
 let pf_compute                   = pf_reduce compute
@@ -92,15 +88,11 @@ let pf_get_type_of               = pf_reduce Retyping.get_type_of
 
 let pf_conv_x                   = pf_reduce is_conv
 let pf_conv_x_leq               = pf_reduce is_conv_leq
-let pf_const_value              = pf_reduce (fun env _ -> constant_value env)
 let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
 let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
 
 let pf_hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls)
 
-let pf_check_type gls c1 c2 =
-  ignore (pf_type_of gls (mkCast (c1, DEFAULTcast, c2)))
-
 let pf_is_matching              = pf_apply ConstrMatching.is_matching_conv
 let pf_matches                  = pf_apply ConstrMatching.matches_conv
 
@@ -140,9 +132,6 @@ let thin_body_no_check ids gl =
 let move_hyp_no_check with_dep id1 id2 gl =
   refiner (Move (with_dep,id1,id2)) gl
 
-let order_hyps idl gl =
-  refiner (Order idl) gl
-
 let rec rename_hyp_no_check l gl = match l with
   | [] -> tclIDTAC gl
   | (id1,id2)::l ->
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 6e4890807..92f8ef829 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -41,9 +41,7 @@ val pf_nth_hyp_id         : goal sigma -> int -> Id.t
 val pf_last_hyp           : goal sigma -> named_declaration
 val pf_ids_of_hyps        : goal sigma -> Id.t list
 val pf_global             : goal sigma -> Id.t -> constr
-val pf_parse_const        : goal sigma -> string -> constr
 val pf_type_of            : goal sigma -> constr -> types
-val pf_check_type         : goal sigma -> constr -> types -> unit
 val pf_hnf_type_of        : goal sigma -> constr -> types
 
 val pf_get_hyp            : goal sigma -> Id.t -> named_declaration
@@ -61,9 +59,7 @@ val pf_reduce :
   goal sigma -> constr -> constr
 
 val pf_whd_betadeltaiota       : goal sigma -> constr -> constr
-val pf_whd_betadeltaiota_stack : goal sigma -> constr -> constr * constr list
 val pf_hnf_constr              : goal sigma -> constr -> constr
-val pf_red_product             : goal sigma -> constr -> constr
 val pf_nf                      : goal sigma -> constr -> constr
 val pf_nf_betaiota             : goal sigma -> constr -> constr
 val pf_reduce_to_quantified_ind : goal sigma -> types -> inductive * types
@@ -72,7 +68,6 @@ val pf_compute                 : goal sigma -> constr -> constr
 val pf_unfoldn    : (occurrences * evaluable_global_reference) list
   -> goal sigma -> constr -> constr
 
-val pf_const_value : goal sigma -> constant -> constr
 val pf_conv_x      : goal sigma -> constr -> constr -> bool
 val pf_conv_x_leq  : goal sigma -> constr -> constr -> bool
 
@@ -85,16 +80,10 @@ val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
 val refiner                   : rule -> tactic
 val introduction_no_check     : Id.t -> tactic
 val internal_cut_no_check     : bool -> Id.t -> types -> tactic
-val internal_cut_rev_no_check : bool -> Id.t -> types -> tactic
 val refine_no_check           : constr -> tactic
 val convert_concl_no_check    : types -> cast_kind -> tactic
 val convert_hyp_no_check      : named_declaration -> tactic
 val thin_no_check             : Id.t list -> tactic
-val thin_body_no_check        : Id.t list -> tactic
-val move_hyp_no_check         :
-  bool -> Id.t -> Id.t move_location -> tactic
-val rename_hyp_no_check       : (Id.t*Id.t) list -> tactic
-val order_hyps : Id.t list -> tactic
 val mutual_fix      :
   Id.t -> int -> (Id.t * int * constr) list -> int -> tactic
 val mutual_cofix    : Id.t -> (Id.t * constr) list -> int -> tactic
@@ -125,7 +114,6 @@ module New : sig
   val pf_env : 'a Proofview.Goal.t -> Environ.env
 
   val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types
-  val pf_get_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types
   val pf_conv_x : 'a Proofview.Goal.t -> Term.constr -> Term.constr -> bool
 
   val pf_get_new_id  : identifier -> [ `NF ] Proofview.Goal.t -> identifier