aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/cc/ccalgo.mli97
-rw-r--r--plugins/funind/indfun_common.ml27
-rw-r--r--plugins/funind/recdef.ml46
-rw-r--r--plugins/syntax/r_syntax.ml2
4 files changed, 31 insertions, 141 deletions
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 3dc934b426..b0b74f4558 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -8,7 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Util
open Constr
open Names
@@ -156,102 +155,6 @@ val subterms : forest -> int -> int * int
val join_path : forest -> int -> int ->
((int * int) * equality) list * ((int * int) * equality) list
-val make_fun_table : state -> Int.Set.t PafMap.t
-
-val do_match : state ->
- (quant_eq * int array) list ref -> matching_problem Stack.t -> unit
-
-val init_pb_stack : state -> matching_problem Stack.t
-
-val paf_of_patt : int Termhash.t -> ccpattern -> pa_fun
-
-val find_instances : state -> (quant_eq * int array) list
-
val execute : bool -> state -> explanation option
val pr_idx_term : Environ.env -> Evd.evar_map -> forest -> int -> Pp.t
-
-val empty_forest: unit -> forest
-
-
-
-
-
-
-
-
-
-
-(*type pa_constructor
-
-
-module PacMap:CSig.MapS with type key=pa_constructor
-
-type term =
- Symb of Term.constr
- | Eps
- | Appli of term * term
- | Constructor of Names.constructor*int*int
-
-type rule =
- Congruence
- | Axiom of Names.Id.t
- | Injection of int*int*int*int
-
-type equality =
- {lhs : int;
- rhs : int;
- rule : rule}
-
-module ST :
-sig
- type t
- val empty : unit -> t
- val enter : int -> int * int -> t -> unit
- val query : int * int -> t -> int
- val delete : int -> t -> unit
- val delete_list : int list -> t -> unit
-end
-
-module UF :
-sig
- type t
- exception Discriminable of int * int * int * int * t
- val empty : unit -> t
- val find : t -> int -> int
- val size : t -> int -> int
- val get_constructor : t -> int -> Names.constructor
- val pac_arity : t -> int -> int * int -> int
- val mem_node_pac : t -> int -> int * int -> int
- val add_pacs : t -> int -> pa_constructor PacMap.t ->
- int list * equality list
- val term : t -> int -> term
- val subterms : t -> int -> int * int
- val add : t -> term -> int
- val union : t -> int -> int -> equality -> int list * equality list
- val join_path : t -> int -> int ->
- ((int*int)*equality) list*
- ((int*int)*equality) list
-end
-
-
-val combine_rec : UF.t -> int list -> equality list
-val process_rec : UF.t -> equality list -> int list
-
-val cc : UF.t -> unit
-
-val make_uf :
- (Names.Id.t * (term * term)) list -> UF.t
-
-val add_one_diseq : UF.t -> (term * term) -> int * int
-
-val add_disaxioms :
- UF.t -> (Names.Id.t * (term * term)) list ->
- (Names.Id.t * (int * int)) list
-
-val check_equal : UF.t -> int * int -> bool
-
-val find_contradiction : UF.t ->
- (Names.Id.t * (int * int)) list ->
- (Names.Id.t * (int * int))
-*)
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 45fafd2872..7d87fc0220 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -92,18 +92,14 @@ let list_union_eq eq_fun l1 l2 =
let list_add_set_eq eq_fun x l =
if List.exists (eq_fun x) l then l else x::l
-[@@@ocaml.warning "-3"]
-let coq_constant s =
- UnivGen.constr_of_monomorphic_global @@
- Coqlib.gen_reference_in_modules "RecursiveDefinition"
- Coqlib.init_modules s;;
+let coq_constant s = UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref s;;
let find_reference sl s =
let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in
Nametab.locate (make_qualid dp (Id.of_string s))
-let eq = lazy(EConstr.of_constr (coq_constant "eq"))
-let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl"))
+let eq = lazy(EConstr.of_constr (coq_constant "core.eq.type"))
+let refl_equal = lazy(EConstr.of_constr (coq_constant "core.eq.refl"))
let with_full_print f a =
let old_implicit_args = Impargs.is_implicit_args ()
@@ -369,10 +365,10 @@ let do_observe_tac s tac g =
ignore(Stack.pop debug_queue);
v
with reraise ->
- let reraise = CErrors.push reraise in
+ let reraise = Exninfo.capture reraise in
if not (Stack.is_empty debug_queue)
then print_debug_queue true (fst reraise);
- Util.iraise reraise
+ Exninfo.iraise reraise
let observe_tac s tac g =
if do_observe ()
@@ -447,14 +443,11 @@ let h_intros l =
let h_id = Id.of_string "h"
let hrec_id = Id.of_string "hrec"
-let well_founded = function () -> EConstr.of_constr (coq_constant "well_founded")
-let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc")
-let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv")
-
-[@@@ocaml.warning "-3"]
-let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@
- Coqlib.find_reference "IndFun" ["Coq"; "Arith";"Wf_nat"] "well_founded_ltof"
-[@@@ocaml.warning "+3"]
+let well_founded = function () -> EConstr.of_constr (coq_constant "core.wf.well_founded")
+let acc_rel = function () -> EConstr.of_constr (coq_constant "core.wf.acc")
+let acc_inv_id = function () -> EConstr.of_constr (coq_constant "core.wf.acc_inv")
+
+let well_founded_ltof () = EConstr.of_constr (coq_constant "num.nat.well_founded_ltof")
let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof")
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index f7f8004998..9fa0ec8c08 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -47,18 +47,12 @@ open Context.Rel.Declaration
(* Ugly things which should not be here *)
-[@@@ocaml.warning "-3"]
-let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@
- Coqlib.find_reference "RecursiveDefinition" m s
-
-let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"]
-let arith_Lt = ["Coq"; "Arith";"Lt"]
+let coq_constant s = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@
+ Coqlib.lib_ref s
let coq_init_constant s =
- EConstr.of_constr (
- UnivGen.constr_of_monomorphic_global @@
- Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s)
-[@@@ocaml.warning "+3"]
+ EConstr.of_constr(UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref s)
+;;
let find_reference sl s =
let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in
@@ -122,26 +116,26 @@ let v_id = Id.of_string "v"
let def_id = Id.of_string "def"
let p_id = Id.of_string "p"
let rec_res_id = Id.of_string "rec_res";;
-let lt = function () -> (coq_init_constant "lt")
-[@@@ocaml.warning "-3"]
-let le = function () -> (Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules "le")
-let ex = function () -> (coq_init_constant "ex")
-let nat = function () -> (coq_init_constant "nat")
+let lt = function () -> (coq_init_constant "num.nat.lt")
+let le = function () -> Coqlib.lib_ref "num.nat.le"
+
+let ex = function () -> (coq_init_constant "core.ex.type")
+let nat = function () -> (coq_init_constant "num.nat.type")
let iter_ref () =
try find_reference ["Recdef"] "iter"
with Not_found -> user_err Pp.(str "module Recdef not loaded")
let iter_rd = function () -> (constr_of_monomorphic_global (delayed_force iter_ref))
-let eq = function () -> (coq_init_constant "eq")
+let eq = function () -> (coq_init_constant "core.eq.type")
let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS")
-let le_lt_n_Sm = function () -> (coq_constant arith_Lt "le_lt_n_Sm")
-let le_trans = function () -> (coq_constant arith_Nat "le_trans")
-let le_lt_trans = function () -> (coq_constant arith_Nat "le_lt_trans")
-let lt_S_n = function () -> (coq_constant arith_Lt "lt_S_n")
-let le_n = function () -> (coq_init_constant "le_n")
+let le_lt_n_Sm = function () -> (coq_constant "num.nat.le_lt_n_Sm")
+let le_trans = function () -> (coq_constant "num.nat.le_trans")
+let le_lt_trans = function () -> (coq_constant "num.nat.le_lt_trans")
+let lt_S_n = function () -> (coq_constant "num.nat.lt_S_n")
+let le_n = function () -> (coq_init_constant "num.nat.le_n")
let coq_sig_ref = function () -> (find_reference ["Coq";"Init";"Specif"] "sig")
-let coq_O = function () -> (coq_init_constant "O")
-let coq_S = function () -> (coq_init_constant "S")
-let lt_n_O = function () -> (coq_constant arith_Nat "nlt_0_r")
+let coq_O = function () -> (coq_init_constant "num.nat.O")
+let coq_S = function () -> (coq_init_constant"num.nat.S")
+let lt_n_O = function () -> (coq_constant "num.nat.nlt_0_r")
let max_ref = function () -> (find_reference ["Recdef"] "max")
let max_constr = function () -> EConstr.of_constr (constr_of_monomorphic_global (delayed_force max_ref))
@@ -817,7 +811,7 @@ let rec prove_le g =
| App (c, [| x0 ; _ |]) ->
EConstr.isVar sigma x0 &&
Id.equal (destVar sigma x0) (destVar sigma x) &&
- EConstr.is_global sigma (le ()) c
+ EConstr.isRefX sigma (le ()) c
| _ -> false
in
let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) in
@@ -1194,7 +1188,7 @@ let get_current_subgoals_types pstate =
exception EmptySubgoals
let build_and_l sigma l =
let and_constr = UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.and.type" in
- let conj_constr = Coqlib.build_coq_conj () in
+ let conj_constr = Coqlib.lib_ref "core.and.conj" in
let mk_and p1 p2 =
mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in
let rec is_well_founded t =
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index f6fbdaa958..fa824a88ee 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -134,7 +134,7 @@ let r_of_rawnum ?loc (sign,n) =
| '+' -> Bigint.of_string (String.sub e 2 (String.length e - 2))
| '-' -> Bigint.(neg (of_string (String.sub e 2 (String.length e - 2))))
| _ -> Bigint.of_string (String.sub e 1 (String.length e - 1)) in
- Bigint.(sub e (of_int (String.length f))) in
+ Bigint.(sub e (of_int (String.length (String.concat "" (String.split_on_char '_' f))))) in
if Bigint.is_strictly_pos e then rmult n (izr (pow10 e))
else if Bigint.is_strictly_neg e then rdiv n (izr (pow10 (neg e)))
else n (* e = 0 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 12:28:55 +0000