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/btauto/refl_btauto.ml5
-rw-r--r--plugins/btauto/refl_btauto.mli11
-rw-r--r--plugins/firstorder/plugin_base.dune2
-rw-r--r--plugins/ltac/profile_ltac.ml2
-rw-r--r--plugins/omega/OmegaLemmas.v8
-rw-r--r--plugins/omega/coq_omega.ml56
-rw-r--r--plugins/omega/coq_omega.mli11
-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
21 files changed, 62 insertions, 199 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/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index ac0a875229..b9ad1ff6d8 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -10,8 +10,6 @@
open Constr
-let contrib_name = "btauto"
-
let bt_lib_constr n = lazy (UnivGen.constr_of_global @@ Coqlib.lib_ref n)
let decomp_term sigma (c : Constr.t) =
@@ -23,7 +21,6 @@ let (===) = Constr.equal
module CoqList = struct
- let typ = bt_lib_constr "core.list.type"
let _nil = bt_lib_constr "core.list.nil"
let _cons = bt_lib_constr "core.list.cons"
@@ -32,12 +29,10 @@ module CoqList = struct
let rec of_list ty = function
| [] -> nil ty
| t::q -> cons ty t (of_list ty q)
- let type_of_list ty = lapp typ [|ty|]
end
module CoqPositive = struct
- let typ = bt_lib_constr "num.pos.type"
let _xH = bt_lib_constr "num.pos.xH"
let _xO = bt_lib_constr "num.pos.xO"
let _xI = bt_lib_constr "num.pos.xI"
diff --git a/plugins/btauto/refl_btauto.mli b/plugins/btauto/refl_btauto.mli
new file mode 100644
index 0000000000..5478fddba5
--- /dev/null
+++ b/plugins/btauto/refl_btauto.mli
@@ -0,0 +1,11 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+module Btauto : sig val tac : unit Proofview.tactic end
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/plugins/omega/OmegaLemmas.v b/plugins/omega/OmegaLemmas.v
index 9593e1225c..81bf1fb83d 100644
--- a/plugins/omega/OmegaLemmas.v
+++ b/plugins/omega/OmegaLemmas.v
@@ -229,17 +229,11 @@ Definition fast_Zmult_comm (x y : Z) (P : Z -> Prop)
Definition fast_Zopp_plus_distr (x y : Z) (P : Z -> Prop)
(H : P (- x + - y)) := eq_ind_r P H (Z.opp_add_distr x y).
-Definition fast_Zopp_involutive (x : Z) (P : Z -> Prop) (H : P x) :=
- eq_ind_r P H (Z.opp_involutive x).
-
Definition fast_Zopp_mult_distr_r (x y : Z) (P : Z -> Prop)
(H : P (x * - y)) := eq_ind_r P H (Zopp_mult_distr_r x y).
Definition fast_Zmult_plus_distr_l (n m p : Z) (P : Z -> Prop)
(H : P (n * p + m * p)) := eq_ind_r P H (Z.mul_add_distr_r n m p).
-Definition fast_Zmult_opp_comm (x y : Z) (P : Z -> Prop)
- (H : P (x * - y)) := eq_ind_r P H (Z.mul_opp_comm x y).
-
Definition fast_Zmult_assoc_reverse (n m p : Z) (P : Z -> Prop)
(H : P (n * (m * p))) := eq_ind_r P H (Zmult_assoc_reverse n m p).
@@ -305,11 +299,9 @@ Register fast_Zred_factor5 as plugins.omega.fast_Zred_factor5.
Register fast_Zred_factor6 as plugins.omega.fast_Zred_factor6.
Register fast_Zmult_plus_distr_l as plugins.omega.fast_Zmult_plus_distr_l.
-Register fast_Zmult_opp_comm as plugins.omega.fast_Zmult_opp_comm.
Register fast_Zopp_plus_distr as plugins.omega.fast_Zopp_plus_distr.
Register fast_Zopp_mult_distr_r as plugins.omega.fast_Zopp_mult_distr_r.
Register fast_Zopp_eq_mult_neg_1 as plugins.omega.fast_Zopp_eq_mult_neg_1.
-Register fast_Zopp_involutive as plugins.omega.fast_Zopp_involutive.
Register new_var as plugins.omega.new_var.
Register intro_Z as plugins.omega.intro_Z.
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index f55458de8d..09bd4cd352 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -42,7 +42,6 @@ let elim_id id = simplest_elim (mkVar id)
let resolve_id id = apply (mkVar id)
-let display_time_flag = ref false
let display_system_flag = ref false
let display_action_flag = ref false
let old_style_flag = ref false
@@ -114,10 +113,6 @@ let new_identifier =
let cpt = intref 0 in
(fun () -> let s = "Omega" ^ string_of_int !cpt in incr cpt; Id.of_string s)
-let new_identifier_state =
- let cpt = intref 0 in
- (fun () -> let s = make_ident "State" (Some !cpt) in incr cpt; s)
-
let new_identifier_var =
let cpt = intref 0 in
(fun () -> let s = "Zvar" ^ string_of_int !cpt in incr cpt; Id.of_string s)
@@ -153,7 +148,6 @@ let mk_then tacs = tclTHENLIST tacs
let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c])
let generalize_tac t = generalize t
-let elim t = simplest_elim t
let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s]
let pf_nf gl c = pf_apply Tacred.simpl gl c
@@ -165,10 +159,9 @@ let rev_assoc k =
in
loop
-let tag_hypothesis,tag_of_hyp, hyp_of_tag, clear_tags =
+let tag_hypothesis, hyp_of_tag, clear_tags =
let l = ref ([]:(Id.t * int) list) in
(fun h id -> l := (h,id):: !l),
- (fun h -> try Id.List.assoc h !l with Not_found -> failwith "tag_hypothesis"),
(fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis"),
(fun () -> l := [])
@@ -259,11 +252,9 @@ let coq_fast_Zred_factor4 = gen_constant "plugins.omega.fast_Zred_factor4"
let coq_fast_Zred_factor5 = gen_constant "plugins.omega.fast_Zred_factor5"
let coq_fast_Zred_factor6 = gen_constant "plugins.omega.fast_Zred_factor6"
let coq_fast_Zmult_plus_distr_l = gen_constant "plugins.omega.fast_Zmult_plus_distr_l"
-let coq_fast_Zmult_opp_comm = gen_constant "plugins.omega.fast_Zmult_opp_comm"
let coq_fast_Zopp_plus_distr = gen_constant "plugins.omega.fast_Zopp_plus_distr"
let coq_fast_Zopp_mult_distr_r = gen_constant "plugins.omega.fast_Zopp_mult_distr_r"
let coq_fast_Zopp_eq_mult_neg_1 = gen_constant "plugins.omega.fast_Zopp_eq_mult_neg_1"
-let coq_fast_Zopp_involutive = gen_constant "plugins.omega.fast_Zopp_involutive"
let coq_Zegal_left = gen_constant "plugins.omega.Zegal_left"
let coq_Zne_left = gen_constant "plugins.omega.Zne_left"
let coq_Zlt_left = gen_constant "plugins.omega.Zlt_left"
@@ -363,23 +354,18 @@ let sp_Zpred = lazy (evaluable_ref_of_constr "Z.pred" coq_Zpred)
let sp_Zminus = lazy (evaluable_ref_of_constr "Z.sub" coq_Zminus)
let sp_Zle = lazy (evaluable_ref_of_constr "Z.le" coq_Zle)
let sp_Zgt = lazy (evaluable_ref_of_constr "Z.gt" coq_Zgt)
-let sp_Zge = lazy (evaluable_ref_of_constr "Z.ge" coq_Zge)
-let sp_Zlt = lazy (evaluable_ref_of_constr "Z.lt" coq_Zlt)
let sp_not = lazy (evaluable_ref_of_constr "not" coq_not)
-let mk_var v = mkVar (Id.of_string v)
let mk_plus t1 t2 = mkApp (Lazy.force coq_Zplus, [| t1; t2 |])
let mk_times t1 t2 = mkApp (Lazy.force coq_Zmult, [| t1; t2 |])
let mk_minus t1 t2 = mkApp (Lazy.force coq_Zminus, [| t1;t2 |])
let mk_gen_eq ty t1 t2 = mkApp (Lazy.force coq_eq, [| ty; t1; t2 |])
let mk_eq t1 t2 = mk_gen_eq (Lazy.force coq_Z) t1 t2
-let mk_le t1 t2 = mkApp (Lazy.force coq_Zle, [| t1; t2 |])
let mk_gt t1 t2 = mkApp (Lazy.force coq_Zgt, [| t1; t2 |])
let mk_inv t = mkApp (Lazy.force coq_Zopp, [| t |])
let mk_and t1 t2 = mkApp (Lazy.force coq_and, [| t1; t2 |])
let mk_or t1 t2 = mkApp (Lazy.force coq_or, [| t1; t2 |])
let mk_not t = mkApp (Lazy.force coq_not, [| t |])
-let mk_eq_rel t1 t2 = mk_gen_eq (Lazy.force coq_comparison) t1 t2
let mk_inj t = mkApp (Lazy.force coq_Z_of_nat, [| t |])
let mk_integer n =
@@ -403,10 +389,6 @@ type omega_constant =
| Le | Lt | Ge | Gt
| Other of string
-type omega_proposition =
- | Keq of constr * constr * constr
- | Kn
-
type result =
| Kvar of Id.t
| Kapp of omega_constant * constr list
@@ -503,12 +485,7 @@ let recognize_number sigma t =
type constr_path =
| P_APP of int
(* Abstraction and product *)
- | P_BODY
| P_TYPE
- (* Case *)
- | P_BRANCH of int
- | P_ARITY
- | P_ARG
let context sigma operation path (t : constr) =
let rec loop i p0 t =
@@ -518,25 +495,10 @@ let context sigma operation path (t : constr) =
| ((P_APP n :: p), App (f,v)) ->
let v' = Array.copy v in
v'.(pred n) <- loop i p v'.(pred n); mkApp (f, v')
- | ((P_BRANCH n :: p), Case (ci,q,c,v)) ->
- (* avant, y avait mkApp... anyway, BRANCH seems nowhere used *)
- let v' = Array.copy v in
- v'.(n) <- loop i p v'.(n); (mkCase (ci,q,c,v'))
- | ((P_ARITY :: p), App (f,l)) ->
- mkApp (loop i p f,l)
- | ((P_ARG :: p), App (f,v)) ->
- let v' = Array.copy v in
- v'.(0) <- loop i p v'.(0); mkApp (f,v')
| (p, Fix ((_,n as ln),(tys,lna,v))) ->
let l = Array.length v in
let v' = Array.copy v in
v'.(n)<- loop (Pervasives.(+) i l) p v.(n); (mkFix (ln,(tys,lna,v')))
- | ((P_BODY :: p), Prod (n,t,c)) ->
- (mkProd (n,t,loop (succ i) p c))
- | ((P_BODY :: p), Lambda (n,t,c)) ->
- (mkLambda (n,t,loop (succ i) p c))
- | ((P_BODY :: p), LetIn (n,b,t,c)) ->
- (mkLetIn (n,b,t,loop (succ i) p c))
| ((P_TYPE :: p), Prod (n,t,c)) ->
(mkProd (n,loop i p t,c))
| ((P_TYPE :: p), Lambda (n,t,c)) ->
@@ -553,13 +515,7 @@ let occurrence sigma path (t : constr) =
| (p, Cast (c,_,_)) -> loop p c
| ([], _) -> t
| ((P_APP n :: p), App (f,v)) -> loop p v.(pred n)
- | ((P_BRANCH n :: p), Case (_,_,_,v)) -> loop p v.(n)
- | ((P_ARITY :: p), App (f,_)) -> loop p f
- | ((P_ARG :: p), App (f,v)) -> loop p v.(0)
| (p, Fix((_,n) ,(_,_,v))) -> loop p v.(n)
- | ((P_BODY :: p), Prod (n,t,c)) -> loop p c
- | ((P_BODY :: p), Lambda (n,t,c)) -> loop p c
- | ((P_BODY :: p), LetIn (n,b,t,c)) -> loop p c
| ((P_TYPE :: p), Prod (n,term,c)) -> loop p term
| ((P_TYPE :: p), Lambda (n,term,c)) -> loop p term
| ((P_TYPE :: p), LetIn (n,b,term,c)) -> loop p term
@@ -584,7 +540,6 @@ let focused_simpl path = focused_simpl path
type oformula =
| Oplus of oformula * oformula
- | Oinv of oformula
| Otimes of oformula * oformula
| Oatom of Id.t
| Oz of bigint
@@ -594,7 +549,6 @@ let rec oprint = function
| Oplus(t1,t2) ->
print_string "("; oprint t1; print_string "+";
oprint t2; print_string ")"
- | Oinv t -> print_string "~"; oprint t
| Otimes (t1,t2) ->
print_string "("; oprint t1; print_string "*";
oprint t2; print_string ")"
@@ -605,7 +559,6 @@ let rec oprint = function
let rec weight = function
| Oatom c -> intern_id c
| Oz _ -> -1
- | Oinv c -> weight c
| Otimes(c,_) -> weight c
| Oplus _ -> failwith "weight"
| Oufo _ -> -1
@@ -613,7 +566,6 @@ let rec weight = function
let rec val_of = function
| Oatom c -> mkVar c
| Oz c -> mk_integer c
- | Oinv c -> mkApp (Lazy.force coq_Zopp, [| val_of c |])
| Otimes (t1,t2) -> mkApp (Lazy.force coq_Zmult, [| val_of t1; val_of t2 |])
| Oplus(t1,t2) -> mkApp (Lazy.force coq_Zplus, [| val_of t1; val_of t2 |])
| Oufo c -> c
@@ -908,10 +860,6 @@ let rec scalar p n = function
clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]]
(Lazy.force coq_fast_Zmult_plus_distr_l) ::
(tac1 @ tac2), Oplus(t1',t2')
- | Oinv t ->
- [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]]
- (Lazy.force coq_fast_Zmult_opp_comm);
- focused_simpl (P_APP 2 :: p)], Otimes(t,Oz(neg n))
| Otimes(t1,Oz x) ->
[clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]]
(Lazy.force coq_fast_Zmult_assoc_reverse);
@@ -963,8 +911,6 @@ let rec negate p = function
(Lazy.force coq_fast_Zopp_plus_distr) ::
(tac1 @ tac2),
Oplus(t1',t2')
- | Oinv t ->
- [clever_rewrite p [[P_APP 1;P_APP 1]] (Lazy.force coq_fast_Zopp_involutive)], t
| Otimes(t1,Oz x) ->
[clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]]
(Lazy.force coq_fast_Zopp_mult_distr_r);
diff --git a/plugins/omega/coq_omega.mli b/plugins/omega/coq_omega.mli
new file mode 100644
index 0000000000..a657826caa
--- /dev/null
+++ b/plugins/omega/coq_omega.mli
@@ -0,0 +1,11 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+val omega_solver : unit Proofview.tactic
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 02:17:26 +0000