Merge PR #8938: [Plugins] Remove some dead code

9 files changed, 9 insertions, 52 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index f26ec0f401..a6f432b5bd 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -333,9 +333,6 @@ let get_representative uf i=
 
 let get_constructors uf i= uf.map.(i).constructors
 
-let find_pac uf i pac =
-  PacMap.find pac (get_constructors uf i)
-
 let rec find_oldest_pac uf i pac=
   try PacMap.find pac (get_constructors uf i) with
     Not_found -> 
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 4ebc6a135a..d52e83dc31 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -145,8 +145,6 @@ val tail_pac : pa_constructor -> pa_constructor
 
 val find : forest -> int -> int
 
-val find_pac : forest -> int -> pa_constructor -> int
-
 val find_oldest_pac : forest -> int -> pa_constructor -> int
 
 val term : forest -> int -> term
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index b9274cf6b8..1128a78093 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -89,8 +89,6 @@ END
 
 {
 
-let fail_solver=tclFAIL 0 (Pp.str "GTauto failed")
-
 let gen_ground_tac flag taco ids bases =
   let backup= !qflag in
   Proofview.tclOR begin
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index b0c4785d7a..832a98b7f8 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -21,7 +21,6 @@ open Termops
 open Formula
 open Sequent
 open Globnames
-open Locus
 
 module NamedDecl = Context.Named.Declaration
 
@@ -56,10 +55,6 @@ let wrap n b continue seq =
     continue seq2
   end
 
-let basename_of_global=function
-    VarRef id->id
-  | _->assert false
-
 let clear_global=function
     VarRef id-> clear [id]
   | _->tclIDTAC
@@ -230,19 +225,3 @@ let ll_forall_tac prod backtrack id continue seq=
     backtrack
 
 (* rules for instantiation with unification moved to instances.ml *)
-
-(* special for compatibility with old Intuition *)
-
-let constant str = Coqlib.lib_ref str
-
-let defined_connectives = lazy
-  [AllOccurrences, EvalConstRef (destConstRef (constant "core.not.type"));
-   AllOccurrences, EvalConstRef (destConstRef (constant "core.iff.type"))]
-
-let normalize_evaluables=
-  Proofview.Goal.enter begin fun gl ->
-    unfold_in_concl (Lazy.force defined_connectives) <*>
-    tclMAP
-      (fun id -> unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly))
-      (pf_ids_of_hyps gl)
-  end
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index 924c26790c..97bc992b26 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -22,8 +22,6 @@ type 'a with_backtracking = tactic -> 'a
 
 val wrap : int -> bool -> seqtac
 
-val basename_of_global: GlobRef.t -> Id.t
-
 val clear_global: GlobRef.t -> tactic
 
 val axiom_tac : constr -> Sequent.t -> tactic
@@ -51,5 +49,3 @@ val forall_tac : seqtac with_backtracking
 val left_exists_tac : pinductive -> lseqtac with_backtracking
 
 val ll_forall_tac : types -> lseqtac with_backtracking
-
-val normalize_evaluables : tactic
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 28a9542167..cd2ea3ef88 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -27,10 +27,6 @@ let array_get_start a =
     (Array.length a - 1)
     (fun i -> a.(i))
 
-let id_of_name = function
-    Name id -> id
-  | _ -> raise Not_found
-
 let locate qid = Nametab.locate qid
 
 let locate_ind ref =
@@ -105,15 +101,6 @@ let const_of_id id =
     CErrors.user_err ~hdr:"IndFun.const_of_id"
       (str "cannot find " ++ Id.print id)
 
-let def_of_const t =
-   match Constr.kind t with
-    Const sp ->
-      (try (match Environ.constant_opt_value_in (Global.env()) sp with
-             | Some c -> c
-	     | _ -> assert false)
-       with Not_found -> assert false)
-    |_ -> assert false
-
 [@@@ocaml.warning "-3"]
 let coq_constant s =
   UnivGen.constr_of_monomorphic_global @@
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 1b4c1248a5..0c8f40c5cf 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -18,8 +18,6 @@ val get_name : Id.t list -> ?default:string -> Name.t -> Name.t
 
 val array_get_start : 'a array -> 'a array
 
-val id_of_name : Name.t -> Id.t
-
 val locate_ind : Libnames.qualid -> inductive
 val locate_constant : Libnames.qualid -> Constant.t
 val locate_with_msg :
@@ -38,7 +36,6 @@ val chop_rlambda_n : int -> Glob_term.glob_constr ->
 val chop_rprod_n : int -> Glob_term.glob_constr ->
   (Name.t*Glob_term.glob_constr) list * Glob_term.glob_constr
 
-val def_of_const : Constr.t -> Constr.t
 val eq : EConstr.constr Lazy.t
 val refl_equal : EConstr.constr Lazy.t
 val const_of_id: Id.t ->  GlobRef.t(* constantyes *)
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 776d2a2229..d90b7d754c 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -34,10 +34,8 @@ let is_gr c gr = match DAst.get c with
 | _ -> false
 
 let positive_modpath = MPfile (make_dir binnums)
-let positive_path = make_path binnums "positive"
 
 let positive_kn = MutInd.make2 positive_modpath (Label.make "positive")
-let glob_positive = IndRef (positive_kn,0)
 let path_of_xI = ((positive_kn,0),1)
 let path_of_xO = ((positive_kn,0),2)
 let path_of_xH = ((positive_kn,0),3)
@@ -71,9 +69,7 @@ let rec bignat_of_pos c = match DAst.get c with
 (* Parsing Z via scopes                                               *)
 (**********************************************************************)
 
-let z_path = make_path binnums "Z"
 let z_kn = MutInd.make2 positive_modpath (Label.make "Z")
-let glob_z = IndRef (z_kn,0)
 let path_of_ZERO = ((z_kn,0),1)
 let path_of_POS = ((z_kn,0),2)
 let path_of_NEG = ((z_kn,0),3)
diff --git a/plugins/syntax/r_syntax.mli b/plugins/syntax/r_syntax.mli
new file mode 100644
index 0000000000..7c3ee60040
--- /dev/null
+++ b/plugins/syntax/r_syntax.mli
@@ -0,0 +1,9 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)