aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/include2
-rw-r--r--dev/top_printers.ml1
-rw-r--r--kernel/univ.ml12
-rw-r--r--plugins/setoid_ring/Ncring_polynom.v4
-rw-r--r--pretyping/evarconv.mli2
-rw-r--r--pretyping/pretyping.ml7
-rw-r--r--pretyping/reductionops.ml32
-rw-r--r--pretyping/reductionops.mli32
-rw-r--r--tactics/rewrite.ml26
-rw-r--r--tactics/tactics.ml3
10 files changed, 66 insertions, 55 deletions
diff --git a/dev/include b/dev/include
index 4a025d077..7c63f5443 100644
--- a/dev/include
+++ b/dev/include
@@ -53,6 +53,8 @@
#install_printer (* type_judgement *) pptype;;
#install_printer (* judgement *) ppj;;
+#install_printer (* judgement *) pp_cst_stack_t;;
+
(*#install_printer (* hint_db *) print_hint_db;;*)
(*#install_printer (* hints_path *) pphintspath;;*)
#install_printer (* goal *) ppgoal;;
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index fb8509c50..fccf580a5 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -140,6 +140,7 @@ let pp_idpred s = pp (pr_idpred s)
let pp_cpred s = pp (pr_cpred s)
let pp_transparent_state s = pp (pr_transparent_state s)
let pp_stack_t n = pp (Reductionops.Stack.pr Termops.print_constr n)
+let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr n)
(* proof printers *)
let pr_evar ev = Pp.int (Evar.repr ev)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index cc1b083d8..3a8724dd5 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -536,6 +536,10 @@ struct
let is_prop = function
| (l,0) -> Level.is_prop l
| _ -> false
+
+ let is_small = function
+ | (l,0) -> Level.is_small l
+ | _ -> false
let equal x y = x == y ||
(let (u,n) = x and (v,n') = y in
@@ -642,8 +646,8 @@ struct
fold (fun x acc -> LSet.add (Expr.get_level x) acc) l LSet.empty
let is_small u =
- match level u with
- | Some l -> Level.is_small l
+ match node u with
+ | Cons (l, n) when is_nil n -> Expr.is_small l
| _ -> false
(* The lower predicative level of the hierarchy that contains (impredicative)
@@ -663,7 +667,9 @@ struct
(* Returns the formal universe that lies juste above the universe variable u.
Used to type the sort u. *)
let super l =
- Huniv.map (fun x -> Expr.successor x) l
+ if is_small l then type1
+ else
+ Huniv.map (fun x -> Expr.successor x) l
let addn n l =
Huniv.map (fun x -> Expr.addn n x) l
diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v
index 32824838b..b0348f8fd 100644
--- a/plugins/setoid_ring/Ncring_polynom.v
+++ b/plugins/setoid_ring/Ncring_polynom.v
@@ -216,8 +216,8 @@ Definition Psub(P P':Pol):= P ++ (--P').
intros l P i n Q;unfold mkPX.
destruct P;try (simpl;reflexivity).
assert (Hh := ring_morphism_eq c 0).
-simpl; case_eq (Ceqb c 0);simpl;try reflexivity.
-intros.
+ simpl; case_eq (Ceqb c 0);simpl;try reflexivity.
+ intros.
rewrite Hh. rewrite ring_morphism0.
rsimpl. apply Ceqb_eq. trivial.
destruct (Pos.compare_spec i p).
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 19175f930..500bb5430 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -65,6 +65,6 @@ val evar_conv_x : transparent_state ->
env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result
val evar_eqappr_x : ?rhs_is_already_stuck:bool -> transparent_state ->
env -> evar_map ->
- conv_pb -> state * constr Cst_stack.t -> state * constr Cst_stack.t ->
+ conv_pb -> state * Cst_stack.t -> state * Cst_stack.t ->
Evarsolve.unification_result
(**/**)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index dff1b9772..cb6deb41c 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -318,11 +318,12 @@ let pretype_ref loc evdref env ref us =
make_judge c ty
let judge_of_Type evd s =
- let judge s =
+ let evd, l = interp_universe_name evd s in
+ let s = Univ.Universe.make l in
+ let judge =
{ uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }
in
- let evd, l = interp_universe_name evd s in
- evd, judge (Univ.Universe.make l)
+ evd, judge
let pretype_sort evdref = function
| GProp -> judge_of_prop
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 74f14aa14..de043aef2 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -141,12 +141,12 @@ module Cst_stack = struct
- constant applied to params = term in head applied to args
- there is at most one arguments with an empty list of args, it must be the first.
- in args, the int represents the indice of the first arg to consider *)
- type 'a t = ('a * 'a list * (int * 'a array) list) list
+ type t = (constr * constr list * (int * constr array) list) list
let empty = []
let sanity x y =
- assert (Constr.equal x y)
+ assert(Term.eq_constr x y)
let drop_useless = function
| _ :: ((_,_,[])::_ as q) -> q
@@ -158,9 +158,9 @@ module Cst_stack = struct
| (c,params,((i,t)::q)) when i = pred (Array.length t) ->
let () = sanity h t.(i) in (c, params, q)
| (c,params,(i,t)::q) ->
- let () = sanity h t.(i) in (c, params, (succ i,t)::q)
- in
- drop_useless (List.map append2cst cst_l)
+ let () = sanity h t.(i) in (c, params, (succ i,t)::q)
+ in
+ drop_useless (List.map append2cst cst_l)
let add_args cl =
List.map (fun (a,b,args) -> (a,b,(0,cl)::args))
@@ -202,10 +202,10 @@ sig
val pr_app_node : ('a -> Pp.std_ppcmds) -> 'a app_node -> Pp.std_ppcmds
type 'a member =
| App of 'a app_node
- | Case of case_info * 'a * 'a array * 'a Cst_stack.t
+ | Case of case_info * 'a * 'a array * Cst_stack.t
| Proj of int * int * projection
- | Fix of fixpoint * 'a t * 'a Cst_stack.t
- | Cst of pconstant * int * int list * 'a t * 'a Cst_stack.t
+ | Fix of fixpoint * 'a t * Cst_stack.t
+ | Cst of pconstant * int * int list * 'a t * Cst_stack.t
| Shift of int
| Update of 'a
and 'a t = 'a member list
@@ -230,7 +230,7 @@ sig
val args_size : 'a t -> int
val tail : int -> 'a t -> 'a t
val nth : 'a t -> int -> 'a
- val best_state : constr * constr t -> constr Cst_stack.t -> constr * constr t
+ val best_state : constr * constr t -> Cst_stack.t -> constr * constr t
val zip : ?refold:bool -> constr * constr t -> constr
end =
struct
@@ -251,10 +251,10 @@ struct
type 'a member =
| App of 'a app_node
- | Case of Term.case_info * 'a * 'a array * 'a Cst_stack.t
+ | Case of Term.case_info * 'a * 'a array * Cst_stack.t
| Proj of int * int * projection
- | Fix of fixpoint * 'a t * 'a Cst_stack.t
- | Cst of pconstant * int * int list * 'a t * 'a Cst_stack.t
+ | Fix of fixpoint * 'a t * Cst_stack.t
+ | Cst of pconstant * int * int list * 'a t * Cst_stack.t
| Shift of int
| Update of 'a
and 'a t = 'a member list
@@ -590,9 +590,9 @@ let apply_subst recfun env cst_l t stack =
aux (h::env) (Cst_stack.add_param h cst_l) c stacktl
| _ -> recfun cst_l (substl env t, stack)
in aux env cst_l t stack
-
+
let stacklam recfun env t stack =
-apply_subst (fun _ -> recfun) env Cst_stack.empty t stack
+ apply_subst (fun _ -> recfun) env Cst_stack.empty t stack
let beta_applist (c,l) =
stacklam Stack.zip [] c (Stack.append_app_list l Stack.empty)
@@ -784,7 +784,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
| Proj (p, c) when Closure.RedFlags.red_set flags (Closure.RedFlags.fCONST p) ->
(match (lookup_constant p env).Declarations.const_proj with
| None -> assert false
- | Some pb -> whrec cst_l (c, Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p)
+ | Some pb -> whrec Cst_stack.empty(* cst_l *) (c, Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p)
:: stack))
| LetIn (_,b,_,c) when Closure.RedFlags.red_set flags Closure.RedFlags.fZETA ->
apply_subst whrec [b] cst_l c stack
@@ -1385,7 +1385,7 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
(Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in
if isConstruct t_o then
if Closure.is_transparent_constant ts p then
- whrec csts_o (Stack.nth stack_o (n+m), stack'')
+ whrec Cst_stack.empty (* csts_o *) (Stack.nth stack_o (n+m), stack'')
else (* Won't unfold *) (whd_betaiota_state sigma (t_o, stack_o@stack'),csts')
else s,csts'
|_, ((Stack.App _| Stack.Shift _|Stack.Update _|Stack.Cst _) :: _|[]) -> s,csts'
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 548517dbf..2ab19c70c 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -34,14 +34,14 @@ end
cst applied to params must convertible to term of the state applied to args
*)
module Cst_stack : sig
- type 'a t
- val empty : 'a t
- val add_param : constr -> constr t -> constr t
- val add_args : 'a array -> 'a t -> 'a t
- val add_cst : 'a -> 'a t -> 'a t
- val best_cst : 'a t -> ('a * 'a list) option
- val best_replace : constr -> constr t -> constr -> constr
- val pr : constr t -> Pp.std_ppcmds
+ type t
+ val empty : t
+ val add_param : constr -> t -> t
+ val add_args : constr array -> t -> t
+ val add_cst : constr -> t -> t
+ val best_cst : t -> (constr * constr list) option
+ val best_replace : constr -> t -> constr -> constr
+ val pr : t -> Pp.std_ppcmds
end
@@ -52,11 +52,11 @@ module Stack : sig
type 'a member =
| App of 'a app_node
- | Case of case_info * 'a * 'a array * 'a Cst_stack.t
+ | Case of case_info * 'a * 'a array * Cst_stack.t
| Proj of int * int * projection
- | Fix of fixpoint * 'a t * 'a Cst_stack.t
+ | Fix of fixpoint * 'a t * Cst_stack.t
| Cst of pconstant * int (** current foccussed arg *) * int list (** remaining args *)
- * 'a t * 'a Cst_stack.t
+ * 'a t * Cst_stack.t
| Shift of int
| Update of 'a
and 'a t = 'a member list
@@ -92,7 +92,7 @@ module Stack : sig
val tail : int -> 'a t -> 'a t
val nth : 'a t -> int -> 'a
- val best_state : constr * constr t -> constr Cst_stack.t -> constr * constr t
+ val best_state : constr * constr t -> Cst_stack.t -> constr * constr t
val zip : ?refold:bool -> constr * constr t -> constr
end
@@ -130,8 +130,8 @@ val stack_reduction_of_reduction :
i*)
val stacklam : (state -> 'a) -> constr list -> constr -> constr Stack.t -> 'a
-val whd_state_gen : ?csts:constr Cst_stack.t -> bool -> Closure.RedFlags.reds ->
- Environ.env -> Evd.evar_map -> state -> state * constr Cst_stack.t
+val whd_state_gen : ?csts:Cst_stack.t -> bool -> Closure.RedFlags.reds ->
+ Environ.env -> Evd.evar_map -> state -> state * Cst_stack.t
val iterate_whd_gen : bool -> Closure.RedFlags.reds ->
Environ.env -> Evd.evar_map -> Term.constr -> Term.constr
@@ -277,8 +277,8 @@ val head_unfold_under_prod : transparent_state -> reduction_function
(** {6 Heuristic for Conversion with Evar } *)
val whd_betaiota_deltazeta_for_iota_state :
- transparent_state -> Environ.env -> Evd.evar_map -> constr Cst_stack.t -> state ->
- state * constr Cst_stack.t
+ transparent_state -> Environ.env -> Evd.evar_map -> Cst_stack.t -> state ->
+ state * Cst_stack.t
(** {6 Meta-related reduction functions } *)
val meta_instance : evar_map -> constr freelisted -> constr
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 2970eece8..b4e1683eb 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -490,13 +490,13 @@ let rec decompose_app_rel env evd t =
let decompose_applied_relation env origsigma sigma flags orig (c,l) left2right =
let c' = c in
- let ctype = Typing.type_of env sigma c' in
+ let ctype = Retyping.get_type_of env sigma c' in
let find_rel ty =
let eqclause = Clenv.make_clenv_binding_env_apply env sigma None (c',ty) l in
let (equiv, args) = decompose_app_rel env eqclause.evd (Clenv.clenv_type eqclause) in
let c1 = args.(0) and c2 = args.(1) in
let ty1, ty2 =
- Typing.type_of env eqclause.evd c1, Typing.type_of env eqclause.evd c2
+ Retyping.get_type_of env eqclause.evd c1, Retyping.get_type_of env eqclause.evd c2
in
if not (evd_convertible env eqclause.evd ty1 ty2) then None
else
@@ -648,8 +648,8 @@ let unify_eqn env (sigma, cstrs) hypinfo by t =
let c1 = nf c1 and c2 = nf c2
and car = nf car and rel = nf rel
and prf = nf prf in
- let ty1 = Typing.type_of env'.env env'.evd c1
- and ty2 = Typing.type_of env'.env env'.evd c2
+ let ty1 = Retyping.get_type_of env'.env env'.evd c1
+ and ty2 = Retyping.get_type_of env'.env env'.evd c2
in
if convertible env env'.evd ty1 ty2 then
(* (if occur_meta_or_existential prf then *)
@@ -925,7 +925,7 @@ let subterm all flags (s : strategy) : strategy =
(fun (acc, evars, progress) arg ->
if not (Option.is_empty progress) && not all then (None :: acc, evars, progress)
else
- let argty = Typing.type_of env (goalevars evars) arg in
+ let argty = Retyping.get_type_of env (goalevars evars) arg in
let res = s env avoid arg argty (prop,None) evars in
match res with
| Some None -> (None :: acc, evars,
@@ -965,7 +965,7 @@ let subterm all flags (s : strategy) : strategy =
in
if flags.on_morphisms then
- let mty = Typing.type_of env (goalevars evars) m in
+ let mty = Retyping.get_type_of env (goalevars evars) m in
let evars, cstr', m, mty, argsl, args =
let argsl = Array.to_list args in
let lift = if prop then PropGlobal.lift_cstr else TypeGlobal.lift_cstr in
@@ -1003,8 +1003,8 @@ let subterm all flags (s : strategy) : strategy =
| Prod (n, x, b) when noccurn 1 b ->
let b = subst1 mkProp b in
- let tx = Typing.type_of env (goalevars evars) x
- and tb = Typing.type_of env (goalevars evars) b in
+ let tx = Retyping.get_type_of env (goalevars evars) x
+ and tb = Retyping.get_type_of env (goalevars evars) b in
let arr = if prop then PropGlobal.arrow_morphism
else TypeGlobal.arrow_morphism
in
@@ -1073,7 +1073,7 @@ let subterm all flags (s : strategy) : strategy =
| Lambda (n, t, b) when flags.under_lambdas ->
let n' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n in
let env' = Environ.push_rel (n', None, t) env in
- let bty = Typing.type_of env' (goalevars evars) b in
+ let bty = Retyping.get_type_of env' (goalevars evars) b in
let unlift = if prop then PropGlobal.unlift_cstr else TypeGlobal.unlift_cstr in
let b' = s env' avoid b bty (prop, unlift env evars cstr) evars in
(match b' with
@@ -1095,7 +1095,7 @@ let subterm all flags (s : strategy) : strategy =
| _ -> b')
| Case (ci, p, c, brs) ->
- let cty = Typing.type_of env (goalevars evars) c in
+ let cty = Retyping.get_type_of env (goalevars evars) c in
let evars', eqty = app_poly_sort prop env evars coq_eq [| cty |] in
let cstr' = Some eqty in
let c' = s env avoid c cty (prop, cstr') evars' in
@@ -1351,7 +1351,7 @@ let rewrite_with flags c left2right loccs : strategy =
let apply_strategy (s : strategy) env avoid concl (prop, cstr) evars =
let res =
- s env avoid concl (Typing.type_of env (goalevars evars) concl)
+ s env avoid concl (Retyping.get_type_of env (goalevars evars) concl)
(prop, Some cstr) evars
in
match res with
@@ -2118,8 +2118,8 @@ let implify id gl =
| (_, None, ty as hd) :: tl when noccurn 1 concl ->
let env = Environ.push_rel_context tl (pf_env gl) in
let sigma = project gl in
- let tyhd = Typing.type_of env sigma ty
- and tyconcl = Typing.type_of (Environ.push_rel hd env) sigma concl in
+ let tyhd = Retyping.get_type_of env sigma ty
+ and tyconcl = Retyping.get_type_of (Environ.push_rel hd env) sigma concl in
let ((sigma,_), app), unfold =
PropGlobal.arrow_morphism env (sigma, Evar.Set.empty) tyhd
(subst1 mkProp tyconcl) ty (subst1 mkProp concl)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 75fe16150..ba389faa9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3828,7 +3828,8 @@ let abstract_subproof id gk tac =
let evd = Evd.merge_universe_subst evd subst in
let open Declareops in
let eff = Safe_typing.sideff_of_con (Global.safe_env ()) cst in
- let effs = cons_side_effects eff no_seff in
+ let effs = cons_side_effects eff
+ Entries.(snd (Future.force const.const_entry_body)) in
let args = List.rev (instance_from_named_context sign) in
let solve = Proofview.V82.tclEVARS evd <*>
Proofview.tclEFFECTS effs <*> new_exact_no_check (applist (lem, args)) in
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 01:54:33 +0000