aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/micromega/certificate.ml4
-rw-r--r--plugins/micromega/mutils.ml39
-rw-r--r--plugins/micromega/mutils.mli8
-rw-r--r--plugins/micromega/persistent_cache.ml27
-rw-r--r--plugins/micromega/persistent_cache.mli10
-rw-r--r--plugins/micromega/polynomial.ml14
-rw-r--r--plugins/micromega/polynomial.mli12
-rw-r--r--plugins/micromega/sos.ml17
-rw-r--r--plugins/micromega/sos_types.ml8
-rw-r--r--plugins/micromega/sos_types.mli8
-rw-r--r--plugins/nsatz/utile.ml109
-rw-r--r--plugins/nsatz/utile.mli13
-rw-r--r--pretyping/nativenorm.ml12
-rw-r--r--test-suite/.csdp.cachebin236597 -> 165200 bytes
-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--vernac/comDefinition.ml32
18 files changed, 28 insertions, 302 deletions
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index e6edd50878..af292c088f 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -514,7 +514,6 @@ let rec scale_term t =
| Zero -> unit_big_int , Zero
| Const n -> (denominator n) , Const (Big_int (numerator n))
| Var n -> unit_big_int , Var n
- | Inv _ -> failwith "scale_term : not implemented"
| Opp t -> let s, t = scale_term t in s, Opp t
| Add(t1,t2) -> let s1,y1 = scale_term t1 and s2,y2 = scale_term t2 in
let g = gcd_big_int s1 s2 in
@@ -530,7 +529,6 @@ let rec scale_term t =
mult_big_int s1 s2 , Mul (y1, y2)
| Pow(t,n) -> let s,t = scale_term t in
power_big_int_positive_int s n , Pow(t,n)
- | _ -> failwith "scale_term : not implemented"
let scale_term t =
let (s,t') = scale_term t in
@@ -572,7 +570,6 @@ let rec term_to_q_expr = function
| Opp p -> PEopp (term_to_q_expr p)
| Pow(t,n) -> PEpow (term_to_q_expr t,Ml2C.n n)
| Sub(t1,t2) -> PEsub (term_to_q_expr t1, term_to_q_expr t2)
- | _ -> failwith "term_to_q_expr: not implemented"
let term_to_q_pol e = Mc.norm_aux (Ml2C.q (Int 0)) (Ml2C.q (Int 1)) Mc.qplus Mc.qmult Mc.qminus Mc.qopp Mc.qeq_bool (term_to_q_expr e)
@@ -610,7 +607,6 @@ let rec term_to_z_expr = function
| Opp p -> PEopp (term_to_z_expr p)
| Pow(t,n) -> PEpow (term_to_z_expr t,Ml2C.n n)
| Sub(t1,t2) -> PEsub (term_to_z_expr t1, term_to_z_expr t2)
- | _ -> failwith "term_to_z_expr: not implemented"
let term_to_z_pol e = Mc.norm_aux (Ml2C.z 0) (Ml2C.z 1) Mc.Z.add Mc.Z.mul Mc.Z.sub Mc.Z.opp Mc.zeq_bool (term_to_z_expr e)
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index 40aeef3959..809731ecc4 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -31,20 +31,12 @@ module IMap =
r
end
-(*let output_int o i = output_string o (string_of_int i)*)
-
-let iset_pp o s =
- Printf.fprintf o "{ %a }"
- (fun o s -> ISet.iter (fun i -> Printf.fprintf o "%i " i) s) s
-
let rec pp_list s f o l =
match l with
| [] -> ()
| [e] -> f o e
| e::l -> f o e ; output_string o s ; pp_list s f o l
-let output_bigint o bi = output_string o (Big_int.string_of_big_int bi)
-
let finally f rst =
try
let res = f () in
@@ -61,16 +53,7 @@ let rec try_any l x =
| None -> try_any l x
| x -> x
-let all_sym_pairs f l =
- let pair_with acc e l = List.fold_left (fun acc x -> (f e x) ::acc) acc l in
-
- let rec xpairs acc l =
- match l with
- | [] -> acc
- | e::l -> xpairs (pair_with acc e l) l in
- xpairs [] l
-
-let all_pairs f l =
+let all_pairs f l =
let pair_with acc e l = List.fold_left (fun acc x -> (f e x) ::acc) acc l in
let rec xpairs acc l =
@@ -123,26 +106,6 @@ let numerator = function
| Int i -> Big_int.big_int_of_int i
| Big_int i -> i
-let rec ppcm_list c l =
- match l with
- | [] -> c
- | e::l -> ppcm_list (ppcm c (denominator e)) l
-
-let rec rec_gcd_list c l =
- match l with
- | [] -> c
- | e::l -> rec_gcd_list (gcd_big_int c (numerator e)) l
-
-let gcd_list l =
- let res = rec_gcd_list zero_big_int l in
- if Int.equal (compare_big_int res zero_big_int) 0
- then unit_big_int else res
-
-let rats_to_ints l =
- let c = ppcm_list unit_big_int l in
- List.map (fun x -> (div_big_int (mult_big_int (numerator x) c)
- (denominator x))) l
-
let iterate_until_stable f x =
let rec iter x =
match f x with
diff --git a/plugins/micromega/mutils.mli b/plugins/micromega/mutils.mli
index 35ca1e5516..e92f086886 100644
--- a/plugins/micromega/mutils.mli
+++ b/plugins/micromega/mutils.mli
@@ -20,10 +20,6 @@ sig
end
-val iset_pp : out_channel -> ISet.t -> unit
-
-val output_bigint : out_channel -> Big_int.big_int -> unit
-
val numerator : Num.num -> Big_int.big_int
val denominator : Num.num -> Big_int.big_int
@@ -73,15 +69,11 @@ module CoqToCaml : sig
end
val ppcm : Big_int.big_int -> Big_int.big_int -> Big_int.big_int
-val rats_to_ints : Num.num list -> Big_int.big_int list
val all_pairs : ('a -> 'a -> 'b) -> 'a list -> 'b list
-val all_sym_pairs : ('a -> 'a -> 'b) -> 'a list -> 'b list
val try_any : (('a -> 'b option) * 'c) list -> 'a -> 'b option
val is_sublist : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
-val gcd_list : Num.num list -> Big_int.big_int
-
val extract : ('a -> 'b option) -> 'a list -> ('b * 'a) option * 'a list
val extract_all : ('a -> 'b option) -> 'a list -> ('b * 'a) list * 'a list
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index ee5a0458e8..0209030b64 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -19,11 +19,6 @@ module type PHashtable =
type 'a t
type key
- val create : int -> string -> 'a t
- (** [create i f] creates an empty persistent table
- with initial size i associated with file [f] *)
-
-
val open_in : string -> 'a t
(** [open_in f] rebuilds a table from the records stored in file [f].
As marshaling is not type-safe, it migth segault.
@@ -37,11 +32,6 @@ module type PHashtable =
(and writes the binding to the file associated with [tbl].)
If [key] is already bound, raises KeyAlreadyBound *)
- val close : 'a t -> unit
- (** [close tbl] is closing the table.
- Once closed, a table cannot be used.
- i.e, find,add will raise UnboundTable *)
-
val memo : string -> (key -> 'a) -> (key -> 'a)
(** [memo cache f] returns a memo function for [f] using file [cache] as persistent table.
Note that the cache will only be loaded when the function is used for the first time *)
@@ -71,14 +61,6 @@ struct
}
-let create i f =
- let flags = [O_WRONLY; O_TRUNC;O_CREAT] in
- {
- outch = out_channel_of_descr (openfile f flags 0o666);
- status = Open ;
- htbl = Table.create i
- }
-
let finally f rst =
try
let res = f () in
@@ -181,15 +163,6 @@ let open_in f =
end
-let close t =
- let {outch = outch ; status = status ; htbl = tbl} = t in
- match t.status with
- | Closed -> () (* don't do it twice *)
- | Open ->
- close_out outch ;
- Table.clear tbl ;
- t.status <- Closed
-
let add t k e =
let {outch = outch ; status = status ; htbl = tbl} = t in
if status == Closed
diff --git a/plugins/micromega/persistent_cache.mli b/plugins/micromega/persistent_cache.mli
index 240fa490fc..4e7a388aaf 100644
--- a/plugins/micromega/persistent_cache.mli
+++ b/plugins/micromega/persistent_cache.mli
@@ -15,11 +15,6 @@ module type PHashtable =
type 'a t
type key
- val create : int -> string -> 'a t
- (** [create i f] creates an empty persistent table
- with initial size i associated with file [f] *)
-
-
val open_in : string -> 'a t
(** [open_in f] rebuilds a table from the records stored in file [f].
As marshaling is not type-safe, it migth segault.
@@ -33,11 +28,6 @@ module type PHashtable =
(and writes the binding to the file associated with [tbl].)
If [key] is already bound, raises KeyAlreadyBound *)
- val close : 'a t -> unit
- (** [close tbl] is closing the table.
- Once closed, a table cannot be used.
- i.e, find,add will raise UnboundTable *)
-
val memo : string -> (key -> 'a) -> (key -> 'a)
(** [memo cache f] returns a memo function for [f] using file [cache] as persistent table.
Note that the cache will only be loaded when the function is used for the first time *)
diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml
index 5f31b6f145..76e7769e82 100644
--- a/plugins/micromega/polynomial.ml
+++ b/plugins/micromega/polynomial.ml
@@ -193,8 +193,6 @@ sig
val addition : t -> t -> t
val uminus : t -> t
val fold : (Monomial.t -> num -> 'a -> 'a) -> t -> 'a -> 'a
- val is_linear : t -> bool
- val variables : t -> ISet.t
val factorise : var -> t -> t * t
end = struct
(*normalisation bug : 0*x ... *)
@@ -259,10 +257,6 @@ end = struct
let fold = P.fold
- let is_linear p = P.fold (fun m _ acc -> acc && (Monomial.is_const m || Monomial.is_var m)) p true
-
- let variables p = P.fold (fun m _ acc -> ISet.union (Monomial.variables m) acc) p ISet.empty
-
let factorise x p =
let x = Monomial.var x in
P.fold (fun m v (px,cx) ->
@@ -294,7 +288,7 @@ let eval_op = function
let string_of_op = function Eq -> "=" | Ge -> ">=" | Gt -> ">"
-let output_cstr o {coeffs = coeffs ; op = op ; cst = cst} =
+let output_cstr o { coeffs ; op ; cst } =
Printf.fprintf o "%a %s %s" Vect.pp coeffs (string_of_op op) (string_of_num cst)
@@ -466,12 +460,6 @@ module LinPoly = struct
end
-let output_nlin_cstr o {coeffs = coeffs ; op = op ; cst = cst} =
- let p = LinPoly.pol_of_linpol coeffs in
-
- Printf.fprintf o "%a %s %s" Poly.pp p (string_of_op op) (string_of_num cst)
-
-
module ProofFormat = struct
open Big_int
diff --git a/plugins/micromega/polynomial.mli b/plugins/micromega/polynomial.mli
index 6f26f7a959..f5e9a9f34c 100644
--- a/plugins/micromega/polynomial.mli
+++ b/plugins/micromega/polynomial.mli
@@ -97,20 +97,10 @@ module Poly : sig
(** [fold f p a] folds f over the monomials of p with non-zero coefficient *)
val fold : (Monomial.t -> Num.num -> 'a -> 'a) -> t -> 'a -> 'a
- (** [is_linear p]
- @return true if the polynomial is of the form a1.x1 +...+ an.xn + c
- i.e every monomial is made of at most a variable *)
- val is_linear : t -> bool
-
-
(** [add m n p]
@return the polynomial n*m + p *)
val add : Monomial.t -> Num.num -> t -> t
- (** [variables p]
- @return the set of variables of the polynomial p *)
- val variables : t -> ISet.t
-
end
type cstr = {coeffs : Vect.t ; op : op ; cst : Num.num} (** Representation of linear constraints *)
@@ -286,8 +276,6 @@ end
val output_cstr : out_channel -> cstr -> unit
-val output_nlin_cstr : out_channel -> cstr -> unit
-
val opMult : op -> op -> op
(** [module WithProof] constructs polynomials packed with the proof that their sign is correct. *)
diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml
index 42a41e176c..f2dfaa42a5 100644
--- a/plugins/micromega/sos.ml
+++ b/plugins/micromega/sos.ml
@@ -145,11 +145,6 @@ let diagonal (v:vector) =
(* ------------------------------------------------------------------------- *)
(* Monomials. *)
(* ------------------------------------------------------------------------- *)
-
-let monomial_eval assig (m:monomial) =
- foldl (fun a x k -> a */ power_num (apply assig x) (Int k))
- (Int 1) m;;
-
let monomial_1 = (undefined:monomial);;
let monomial_var x = (x |=> 1 :monomial);;
@@ -166,10 +161,6 @@ let monomial_variables m = dom m;;
(* ------------------------------------------------------------------------- *)
(* Polynomials. *)
(* ------------------------------------------------------------------------- *)
-
-let eval assig (p:poly) =
- foldl (fun a m c -> a +/ c */ monomial_eval assig m) (Int 0) p;;
-
let poly_0 = (undefined:poly);;
let poly_isconst (p:poly) = foldl (fun a m c -> m = monomial_1 && a) true p;;
@@ -289,17 +280,9 @@ let rec poly_of_term t = match t with
| Const n -> poly_const n
| Var x -> poly_var x
| Opp t1 -> poly_neg (poly_of_term t1)
-| Inv t1 ->
- let p = poly_of_term t1 in
- if poly_isconst p then poly_const(Int 1 // eval undefined p)
- else failwith "poly_of_term: inverse of non-constant polyomial"
| Add (l, r) -> poly_add (poly_of_term l) (poly_of_term r)
| Sub (l, r) -> poly_sub (poly_of_term l) (poly_of_term r)
| Mul (l, r) -> poly_mul (poly_of_term l) (poly_of_term r)
-| Div (l, r) ->
- let p = poly_of_term l and q = poly_of_term r in
- if poly_isconst q then poly_cmul (Int 1 // eval undefined q) p
- else failwith "poly_of_term: division by non-constant polynomial"
| Pow (t, n) ->
poly_pow (poly_of_term t) n;;
diff --git a/plugins/micromega/sos_types.ml b/plugins/micromega/sos_types.ml
index dde1e6c0b0..79d67b6ae9 100644
--- a/plugins/micromega/sos_types.ml
+++ b/plugins/micromega/sos_types.ml
@@ -11,19 +11,17 @@
(* The type of positivstellensatz -- used to communicate with sos *)
open Num
-type vname = string;;
+type vname = string
type term =
| Zero
| Const of Num.num
| Var of vname
-| Inv of term
| Opp of term
| Add of (term * term)
| Sub of (term * term)
| Mul of (term * term)
-| Div of (term * term)
-| Pow of (term * int);;
+| Pow of (term * int)
let rec output_term o t =
@@ -31,12 +29,10 @@ let rec output_term o t =
| Zero -> output_string o "0"
| Const n -> output_string o (string_of_num n)
| Var n -> Printf.fprintf o "v%s" n
- | Inv t -> Printf.fprintf o "1/(%a)" output_term t
| Opp t -> Printf.fprintf o "- (%a)" output_term t
| Add(t1,t2) -> Printf.fprintf o "(%a)+(%a)" output_term t1 output_term t2
| Sub(t1,t2) -> Printf.fprintf o "(%a)-(%a)" output_term t1 output_term t2
| Mul(t1,t2) -> Printf.fprintf o "(%a)*(%a)" output_term t1 output_term t2
- | Div(t1,t2) -> Printf.fprintf o "(%a)/(%a)" output_term t1 output_term t2
| Pow(t1,i) -> Printf.fprintf o "(%a)^(%i)" output_term t1 i
(* ------------------------------------------------------------------------- *)
(* Data structure for Positivstellensatz refutations. *)
diff --git a/plugins/micromega/sos_types.mli b/plugins/micromega/sos_types.mli
index 050ff1e4f7..aa5fb08489 100644
--- a/plugins/micromega/sos_types.mli
+++ b/plugins/micromega/sos_types.mli
@@ -10,19 +10,17 @@
(* The type of positivstellensatz -- used to communicate with sos *)
-type vname = string;;
+type vname = string
type term =
| Zero
| Const of Num.num
| Var of vname
-| Inv of term
| Opp of term
| Add of (term * term)
| Sub of (term * term)
| Mul of (term * term)
-| Div of (term * term)
-| Pow of (term * int);;
+| Pow of (term * int)
val output_term : out_channel -> term -> unit
@@ -37,6 +35,6 @@ type positivstellensatz =
| Monoid of int list
| Eqmul of term * positivstellensatz
| Sum of positivstellensatz * positivstellensatz
- | Product of positivstellensatz * positivstellensatz;;
+ | Product of positivstellensatz * positivstellensatz
val output_psatz : out_channel -> positivstellensatz -> unit
diff --git a/plugins/nsatz/utile.ml b/plugins/nsatz/utile.ml
index d3cfd75e56..1caa042db6 100644
--- a/plugins/nsatz/utile.ml
+++ b/plugins/nsatz/utile.ml
@@ -3,116 +3,7 @@
let pr x =
if !Flags.debug then (Format.printf "@[%s@]" x; flush(stdout);)else ()
-let prn x =
- if !Flags.debug then (Format.printf "@[%s\n@]" x; flush(stdout);) else ()
-
let prt0 s = () (* print_string s;flush(stdout)*)
-let prt s =
- if !Flags.debug then (print_string (s^"\n");flush(stdout)) else ()
-
let sinfo s = if !Flags.debug then Feedback.msg_debug (Pp.str s)
let info s = if !Flags.debug then Feedback.msg_debug (Pp.str (s ()))
-
-(* Lists *)
-
-let rec list_mem_eq eq x l =
- match l with
- [] -> false
- |y::l1 -> if (eq x y) then true else (list_mem_eq eq x l1)
-
-let set_of_list_eq eq l =
- let res = ref [] in
- List.iter (fun x -> if not (list_mem_eq eq x (!res)) then res:=x::(!res)) l;
- List.rev !res
-
-(**********************************************************************
- Eléments minimaux pour un ordre partiel de division.
- E est un ensemble, avec une multiplication
- et une division partielle div (la fonction div peut échouer),
- constant est un prédicat qui définit un sous-ensemble C de E.
-*)
-(*
- Etant donnée une partie A de E, on calcule une partie B de E disjointe de C
- telle que:
- - les éléments de A sont des produits d'éléments de B et d'un de C.
- - B est minimale pour cette propriété.
-*)
-
-let facteurs_liste div constant lp =
- let lp = List.filter (fun x -> not (constant x)) lp in
- let rec factor lmin lp = (* lmin: ne se divisent pas entre eux *)
- match lp with
- [] -> lmin
- |p::lp1 ->
- (let l1 = ref [] in
- let p_dans_lmin = ref false in
- List.iter (fun q -> try (let r = div p q in
- if not (constant r)
- then l1:=r::(!l1)
- else p_dans_lmin:=true)
- with e when CErrors.noncritical e -> ())
- lmin;
- if !p_dans_lmin
- then factor lmin lp1
- else if (!l1)=[]
- (* aucun q de lmin ne divise p *)
- then (let l1=ref lp1 in
- let lmin1=ref [] in
- List.iter (fun q -> try (let r = div q p in
- if not (constant r)
- then l1:=r::(!l1))
- with e when CErrors.noncritical e ->
- lmin1:=q::(!lmin1))
- lmin;
- factor (List.rev (p::(!lmin1))) !l1)
- (* au moins un q de lmin divise p non trivialement *)
- else factor lmin ((!l1)@lp1))
- in
- factor [] lp
-
-
-(* On suppose que tout élément de A est produit d'éléments de B et d'un de C:
- A et B sont deux tableaux, rend un tableau de couples
- (élément de C, listes d'indices l)
- tels que A.(i) = l.(i)_1*Produit(B.(j), j dans l.(i)_2)
- zero est un prédicat sur E tel que (zero x) => (constant x):
- si (zero x) est vrai on ne decompose pas x
- c est un élément quelconque de E.
-*)
-let factorise_tableau div zero c f l1 =
- let res = Array.make (Array.length f) (c,[]) in
- Array.iteri (fun i p ->
- let r = ref p in
- let li = ref [] in
- if not (zero p)
- then
- Array.iteri (fun j q ->
- try (while true do
- let rr = div !r q in
- li:=j::(!li);
- r:=rr;
- done)
- with e when CErrors.noncritical e -> ())
- l1;
- res.(i)<-(!r,!li))
- f;
- (l1,res)
-
-
-(* exemples:
-
-let l = [1;2;6;24;720]
-and div1 = (fun a b -> if a mod b =0 then a/b else failwith "div")
-and constant = (fun x -> x<2)
-and zero = (fun x -> x=0)
-
-
-let f = facteurs_liste div1 constant l
-
-
-factorise_tableau div1 zero 0 (Array.of_list l) (Array.of_list f)
-
-*)
-
-
diff --git a/plugins/nsatz/utile.mli b/plugins/nsatz/utile.mli
index 9308577e0f..5af7ece5a3 100644
--- a/plugins/nsatz/utile.mli
+++ b/plugins/nsatz/utile.mli
@@ -1,19 +1,6 @@
(* Printing *)
val pr : string -> unit
-val prn : string -> unit
val prt0 : 'a -> unit
-val prt : string -> unit
val info : (unit -> string) -> unit
val sinfo : string -> unit
-
-(* Listes *)
-val list_mem_eq : ('a -> 'b -> bool) -> 'a -> 'b list -> bool
-val set_of_list_eq : ('a -> 'a -> bool) -> 'a list -> 'a list
-
-
-val facteurs_liste : ('a -> 'a -> 'a) -> ('a -> bool) -> 'a list -> 'a list
-val factorise_tableau :
- ('a -> 'b -> 'a) ->
- ('a -> bool) ->
- 'a -> 'a array -> 'b array -> 'b array * ('a * int list) array
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/.csdp.cache b/test-suite/.csdp.cache
index bd88c06d11..b85258505b 100644
--- a/test-suite/.csdp.cache
+++ b/test-suite/.csdp.cache
Binary files differ
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/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-04-29 20:01:30 +0000