aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--clib/cArray.ml40
-rw-r--r--clib/cArray.mli10
-rw-r--r--clib/cString.ml33
-rw-r--r--clib/cString.mli6
-rw-r--r--ide/coqide.ml2
-rw-r--r--ide/preferences.ml2
-rw-r--r--lib/envars.ml2
-rw-r--r--plugins/firstorder/plugin_base.dune2
-rw-r--r--plugins/ltac/profile_ltac.ml2
-rw-r--r--pretyping/nativenorm.ml12
-rw-r--r--test-suite/bugs/closed/bug_3690.v7
-rw-r--r--test-suite/bugs/closed/bug_3956.v8
-rw-r--r--test-suite/bugs/closed/bug_7631.v2
-rw-r--r--tools/coq_makefile.ml6
-rw-r--r--toplevel/coqargs.ml4
-rw-r--r--vernac/comDefinition.ml32
16 files changed, 39 insertions, 131 deletions
diff --git a/clib/cArray.ml b/clib/cArray.ml
index d3fa4ef65e..9644834381 100644
--- a/clib/cArray.ml
+++ b/clib/cArray.ml
@@ -17,9 +17,7 @@ sig
val equal : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
val equal_norefl : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
val is_empty : 'a array -> bool
- val exists : ('a -> bool) -> 'a array -> bool
val exists2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool
- val for_all : ('a -> bool) -> 'a array -> bool
val for_all2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool
val for_all3 : ('a -> 'b -> 'c -> bool) ->
'a array -> 'b array -> 'c array -> bool
@@ -49,12 +47,10 @@ sig
val map_to_list : ('a -> 'b) -> 'a array -> 'b list
val map_of_list : ('a -> 'b) -> 'a list -> 'b array
val chop : int -> 'a array -> 'a array * 'a array
- val map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
val map2_i : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
val map3 :
('a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array
val map_left : ('a -> 'b) -> 'a array -> 'b array
- val iter2 : ('a -> 'b -> unit) -> 'a array -> 'b array -> unit
val iter2_i : (int -> 'a -> 'b -> unit) -> 'a array -> 'b array -> unit
val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array
val fold_right_map : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c
@@ -126,13 +122,6 @@ let equal cmp t1 t2 =
let is_empty array = Int.equal (Array.length array) 0
-let exists f v =
- let rec exrec = function
- | -1 -> false
- | n -> f (uget v n) || (exrec (n-1))
- in
- exrec ((Array.length v)-1)
-
let exists2 f v1 v2 =
let rec exrec = function
| -1 -> false
@@ -141,15 +130,6 @@ let exists2 f v1 v2 =
let lv1 = Array.length v1 in
lv1 = Array.length v2 && exrec (lv1-1)
-let for_all f v =
- let rec allrec = function
- | -1 -> true
- | n ->
- let ans = f (uget v n) in
- ans && (allrec (n-1))
- in
- allrec ((Array.length v)-1)
-
let for_all2 f v1 v2 =
let rec allrec = function
| -1 -> true
@@ -336,20 +316,6 @@ let chop n v =
if n > vlen then failwith "Array.chop";
(Array.sub v 0 n, Array.sub v n (vlen-n))
-let map2 f v1 v2 =
- let len1 = Array.length v1 in
- let len2 = Array.length v2 in
- let () = if not (Int.equal len1 len2) then invalid_arg "Array.map2" in
- if Int.equal len1 0 then
- [| |]
- else begin
- let res = Array.make len1 (f (uget v1 0) (uget v2 0)) in
- for i = 1 to pred len1 do
- Array.unsafe_set res i (f (uget v1 i) (uget v2 i))
- done;
- res
- end
-
let map2_i f v1 v2 =
let len1 = Array.length v1 in
let len2 = Array.length v2 in
@@ -390,12 +356,6 @@ let map_left f a = (* Ocaml does not guarantee Array.map is LR *)
r
end
-let iter2 f v1 v2 =
- let len1 = Array.length v1 in
- let len2 = Array.length v2 in
- let () = if not (Int.equal len2 len1) then invalid_arg "Array.iter2" in
- for i = 0 to len1 - 1 do f (uget v1 i) (uget v2 i) done
-
let iter2_i f v1 v2 =
let len1 = Array.length v1 in
let len2 = Array.length v2 in
diff --git a/clib/cArray.mli b/clib/cArray.mli
index f5b015b206..e65a56d15e 100644
--- a/clib/cArray.mli
+++ b/clib/cArray.mli
@@ -27,12 +27,8 @@ sig
val is_empty : 'a array -> bool
(** True whenever the array is empty. *)
- val exists : ('a -> bool) -> 'a array -> bool
- (** As [List.exists] but on arrays. *)
-
val exists2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool
- val for_all : ('a -> bool) -> 'a array -> bool
val for_all2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool
val for_all3 : ('a -> 'b -> 'c -> bool) ->
'a array -> 'b array -> 'c array -> bool
@@ -82,9 +78,6 @@ sig
(** [chop i a] returns [(a1, a2)] s.t. [a = a1 + a2] and [length a1 = n].
Raise [Failure "Array.chop"] if [i] is not a valid index. *)
- val map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
- (** See also [Smart.map2] *)
-
val map2_i : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
val map3 :
('a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array
@@ -92,9 +85,6 @@ sig
val map_left : ('a -> 'b) -> 'a array -> 'b array
(** As [map] but guaranteed to be left-to-right. *)
- val iter2 : ('a -> 'b -> unit) -> 'a array -> 'b array -> unit
- (** Iter on two arrays. Raise [Invalid_argument "Array.iter2"] if sizes differ. *)
-
val iter2_i : (int -> 'a -> 'b -> unit) -> 'a array -> 'b array -> unit
(** Iter on two arrays. Raise [Invalid_argument "Array.iter2_i"] if sizes differ. *)
diff --git a/clib/cString.ml b/clib/cString.ml
index b178cbbd2c..111be3da82 100644
--- a/clib/cString.ml
+++ b/clib/cString.ml
@@ -18,6 +18,7 @@ sig
val explode : string -> string list
val implode : string list -> string
val strip : string -> string
+ [@@ocaml.deprecated "Use [trim]"]
val drop_simple_quotes : string -> string
val string_index_from : string -> int -> string -> int
val string_contains : where:string -> what:string -> bool
@@ -25,6 +26,7 @@ sig
val conjugate_verb_to_be : int -> string
val ordinal : int -> string
val split : char -> string -> string list
+ [@@ocaml.deprecated "Use [split_on_char]"]
val is_sub : string -> string -> int -> bool
module Set : Set.S with type elt = t
module Map : CMap.ExtS with type key = t and module Set := Set
@@ -55,26 +57,9 @@ let explode s =
let implode sl = String.concat "" sl
-let is_blank = function
- | ' ' | '\r' | '\t' | '\n' -> true
- | _ -> false
-
let is_empty s = String.length s = 0
-let strip s =
- let n = String.length s in
- let rec lstrip_rec i =
- if i < n && is_blank s.[i] then
- lstrip_rec (i+1)
- else i
- in
- let rec rstrip_rec i =
- if i >= 0 && is_blank s.[i] then
- rstrip_rec (i-1)
- else i
- in
- let a = lstrip_rec 0 and b = rstrip_rec (n-1) in
- String.sub s a (b-a+1)
+let strip = String.trim
let drop_simple_quotes s =
let n = String.length s in
@@ -139,17 +124,7 @@ let ordinal n =
(* string parsing *)
-let split c s =
- let len = String.length s in
- let rec split n =
- try
- let pos = String.index_from s n c in
- let dir = String.sub s n (pos-n) in
- dir :: split (succ pos)
- with
- | Not_found -> [String.sub s n (len-n)]
- in
- if Int.equal len 0 then [] else split 0
+let split = String.split_on_char
module Self =
struct
diff --git a/clib/cString.mli b/clib/cString.mli
index df25a3821a..a73c2729d0 100644
--- a/clib/cString.mli
+++ b/clib/cString.mli
@@ -31,7 +31,8 @@ sig
(** [implode [s1; ...; sn]] returns [s1 ^ ... ^ sn] *)
val strip : string -> string
- (** Remove the surrounding blank characters from a string *)
+ (** Alias for [String.trim] *)
+ [@@ocaml.deprecated "Use [trim]"]
val drop_simple_quotes : string -> string
(** Remove the eventual first surrounding simple quotes of a string. *)
@@ -52,7 +53,8 @@ sig
(** Generate the ordinal number in English. *)
val split : char -> string -> string list
- (** [split c s] splits [s] into sequences separated by [c], excluded. *)
+ (** [split c s] alias of [String.split_on_char] *)
+ [@@ocaml.deprecated "Use [split_on_char]"]
val is_sub : string -> string -> int -> bool
(** [is_sub p s off] tests whether [s] contains [p] at offset [off]. *)
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 00d43e6e64..4190f43680 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -769,7 +769,7 @@ let coqtop_arguments sn =
let box = dialog#action_area in
let ok = GButton.button ~stock:`OK ~packing:box#add () in
let ok_cb () =
- let nargs = CString.split ' ' entry#text in
+ let nargs = String.split_on_char ' ' entry#text in
if nargs <> args then
let failed = Coq.filter_coq_opts nargs in
match failed with
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 9f04ced1c3..6dc922c225 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -167,7 +167,7 @@ object
method into l =
try
Some (CList.map (fun s ->
- let split = CString.split sep s in
+ let split = String.split_on_char sep s in
CList.nth split 0, CList.nth split 1) l)
with Failure _ -> None
end
diff --git a/lib/envars.ml b/lib/envars.ml
index cf76b6ebc8..724a3dddc7 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -34,7 +34,7 @@ let home ~warn =
let path_to_list p =
let sep = if String.equal Sys.os_type "Win32" then ';' else ':' in
- String.split sep p
+ String.split_on_char sep p
let expand_path_macros ~warn s =
let rec expand_atom s i =
diff --git a/plugins/firstorder/plugin_base.dune b/plugins/firstorder/plugin_base.dune
index bcbb99d9fc..d88daa23fc 100644
--- a/plugins/firstorder/plugin_base.dune
+++ b/plugins/firstorder/plugin_base.dune
@@ -1,5 +1,5 @@
(library
(name ground_plugin)
- (public_name coq.plugins.ground)
+ (public_name coq.plugins.firstorder)
(synopsis "Coq's first order logic solver plugin")
(libraries coq.plugins.ltac))
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index d22bd4967a..db7dcfa6ef 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -260,7 +260,7 @@ let string_of_call ck =
) in
let s = String.map (fun c -> if c = '\n' then ' ' else c) s in
let s = try String.sub s 0 (CString.string_index_from s 0 "(*") with Not_found -> s in
- CString.strip s
+ String.trim s
let rec merge_sub_tree name tree acc =
try
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 20185363e6..022c383f60 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -132,15 +132,15 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs =
(mkApp(mkConstructU((ind,i),u), params), ctyp)
-let construct_of_constr const env tag typ =
+let construct_of_constr const env sigma tag typ =
let t, l = app_type env typ in
- match kind t with
+ match EConstr.kind_upto sigma t with
| Ind (ind,u) ->
construct_of_constr_notnative const env tag ind u l
| _ -> assert false
-let construct_of_constr_const env tag typ =
- fst (construct_of_constr true env tag typ)
+let construct_of_constr_const env sigma tag typ =
+ fst (construct_of_constr true env sigma tag typ)
let construct_of_constr_block = construct_of_constr false
@@ -207,9 +207,9 @@ let rec nf_val env sigma v typ =
let env = push_rel (LocalAssum (name,dom)) env in
let body = nf_val env sigma (f (mk_rel_accu lvl)) codom in
mkLambda(name,dom,body)
- | Vconst n -> construct_of_constr_const env n typ
+ | Vconst n -> construct_of_constr_const env sigma n typ
| Vblock b ->
- let capp,ctyp = construct_of_constr_block env (block_tag b) typ in
+ let capp,ctyp = construct_of_constr_block env sigma (block_tag b) typ in
let args = nf_bargs env sigma b ctyp in
mkApp(capp,args)
diff --git a/test-suite/bugs/closed/bug_3690.v b/test-suite/bugs/closed/bug_3690.v
index fa30132ab5..9273a20e19 100644
--- a/test-suite/bugs/closed/bug_3690.v
+++ b/test-suite/bugs/closed/bug_3690.v
@@ -41,8 +41,5 @@ Type@{Top.34} -> Type@{Top.37}
Top.36 < Top.34
Top.37 < Top.36
*) *)
-Fail Check @qux@{Set Set}.
-Check @qux@{Type Type Type Type}.
-(* [qux] should only need two universes *)
-Check @qux@{i j k l}. (* Error: The command has not failed!, but I think this is suboptimal *)
-Fail Check @qux@{i j}.
+Check @qux@{Type Type}.
+(* used to have 4 universes *)
diff --git a/test-suite/bugs/closed/bug_3956.v b/test-suite/bugs/closed/bug_3956.v
index 115284ec02..456fa11bd0 100644
--- a/test-suite/bugs/closed/bug_3956.v
+++ b/test-suite/bugs/closed/bug_3956.v
@@ -129,13 +129,13 @@ Module Comodality_Theory (F : Comodality).
:= IdmapM FPM.
Module cip_FPM := FPM.coindpathsM FPM cmpinv_o_cmp_M idmap_FPM.
Module cip_FPHM <: HomotopyM FPM cmpM.PM cip_FPM.fhM cip_FPM.fkM.
- Definition m : forall x, cip_FPM.fhM.m@{i j} x = cip_FPM.fkM.m@{i j} x.
+ Definition m : forall x, cip_FPM.fhM.m x = cip_FPM.fkM.m x.
Proof.
intros x.
- refine (concat (cmpinvM.m_beta@{i j} (cmpM.m@{i j} x)) _).
+ refine (concat (cmpinvM.m_beta (cmpM.m x)) _).
apply path_prod@{i i i}; simpl.
- - exact (cmpM.FfstM.mM.m_beta@{i j} x).
- - exact (cmpM.FsndM.mM.m_beta@{i j} x).
+ - exact (cmpM.FfstM.mM.m_beta x).
+ - exact (cmpM.FsndM.mM.m_beta x).
Defined.
End cip_FPHM.
End isequiv_F_prod_cmp_M.
diff --git a/test-suite/bugs/closed/bug_7631.v b/test-suite/bugs/closed/bug_7631.v
index 34eb8b8676..93aeb83e28 100644
--- a/test-suite/bugs/closed/bug_7631.v
+++ b/test-suite/bugs/closed/bug_7631.v
@@ -7,6 +7,7 @@ Section Foo.
Let bar := foo.
Eval native_compute in bar.
+Eval vm_compute in bar.
End Foo.
@@ -17,5 +18,6 @@ Module RelContext.
Definition foo := true.
Definition bar (x := foo) := Eval native_compute in x.
+Definition barvm (x := foo) := Eval vm_compute in x.
End RelContext.
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 0e56cc3c0f..d91c4f0b34 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -248,7 +248,7 @@ let rec logic_gcd acc = function
let generate_conf_doc oc { defs; q_includes; r_includes } =
let includes = List.map (forget_source > snd) (q_includes @ r_includes) in
- let logpaths = List.map (CString.split '.') includes in
+ let logpaths = List.map (String.split_on_char '.') includes in
let gcd = logic_gcd [] logpaths in
let root =
if gcd = [] then
@@ -378,8 +378,8 @@ let destination_of { ml_includes; q_includes; r_includes; } file =
| _ -> assert false
let share_prefix s1 s2 =
- let s1 = CString.split '.' s1 in
- let s2 = CString.split '.' s2 in
+ let s1 = String.split_on_char '.' s1 in
+ let s2 = String.split_on_char '.' s2 in
match s1, s2 with
| x :: _ , y :: _ -> x = y
| _ -> false
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 06d9ba3436..9918adfed3 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -244,7 +244,7 @@ let get_float opt n =
prerr_endline ("Error: float expected after option "^opt); exit 1
let get_host_port opt s =
- match CString.split ':' s with
+ match String.split_on_char ':' s with
| [host; portr; portw] ->
Some (Spawned.Socket(host, int_of_string portr, int_of_string portw))
| ["stdfds"] -> Some Spawned.AnonPipe
@@ -255,7 +255,7 @@ let get_host_port opt s =
let get_error_resilience opt = function
| "on" | "all" | "yes" -> `All
| "off" | "no" -> `None
- | s -> `Only (CString.split ',' s)
+ | s -> `Only (String.split_on_char ',' s)
let get_priority opt s =
try CoqworkmgrApi.priority_of_string s
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 5d17662d1a..cc03473bc6 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -10,39 +10,19 @@
open Pp
open Util
-open Constr
-open Environ
open Entries
open Redexpr
open Declare
open Constrintern
open Pretyping
-open Context.Rel.Declaration
-
(* Commands of the interface: Constant definitions *)
-let rec under_binders env sigma f n c =
- if Int.equal n 0 then f env sigma (EConstr.of_constr c) else
- match Constr.kind c with
- | Lambda (x,t,c) ->
- mkLambda (x,t,under_binders (push_rel (LocalAssum (x,t)) env) sigma f (n-1) c)
- | LetIn (x,b,t,c) ->
- mkLetIn (x,b,t,under_binders (push_rel (LocalDef (x,b,t)) env) sigma f (n-1) c)
- | _ -> assert false
-
-let red_constant_entry n ce sigma = function
- | None -> ce
+let red_constant_body red_opt env sigma body = match red_opt with
+ | None -> sigma, body
| Some red ->
- let proof_out = ce.const_entry_body in
- let env = Global.env () in
- let (redfun, _) = reduction_of_red_expr env red in
- let redfun env sigma c =
- let (_, c) = redfun env sigma c in
- EConstr.Unsafe.to_constr c
- in
- { ce with const_entry_body = Future.chain proof_out
- (fun ((body,ctx),eff) -> (under_binders env sigma redfun n body,ctx),eff) }
+ let red, _ = reduction_of_red_expr env red in
+ red env sigma body
let warn_implicits_in_term =
CWarnings.create ~name:"implicits-in-term" ~category:"implicits"
@@ -84,6 +64,8 @@ let interp_definition pl bl poly red_option c ctypopt =
check_imps ~impsty ~impsbody;
evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsty, Some ty
in
+ (* Do the reduction *)
+ let evd, c = red_constant_body red_option env_bl evd c in
(* universe minimization *)
let evd = Evd.minimize_universes evd in
(* Substitute evars and universes, and add parameters.
@@ -101,7 +83,7 @@ let interp_definition pl bl poly red_option c ctypopt =
let uctx = Evd.check_univ_decl ~poly evd decl in
(* We're done! *)
let ce = definition_entry ?types:tyopt ~univs:uctx c in
- (red_constant_entry (Context.Rel.length ctx) ce evd red_option, evd, decl, imps)
+ (ce, evd, decl, imps)
let check_definition (ce, evd, _, imps) =
let env = Global.env () in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 09:01:24 +0000