aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/cc/ccalgo.ml3
-rw-r--r--plugins/cc/ccalgo.mli2
-rw-r--r--plugins/firstorder/g_ground.mlg2
-rw-r--r--plugins/firstorder/rules.ml21
-rw-r--r--plugins/firstorder/rules.mli4
-rw-r--r--plugins/funind/indfun_common.ml13
-rw-r--r--plugins/funind/indfun_common.mli3
-rw-r--r--plugins/syntax/r_syntax.ml4
-rw-r--r--plugins/syntax/r_syntax.mli9
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) *)
+(************************************************************************)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:49:24 +0000