aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/sphinx/proofs/writing-proofs/rewriting.rst6
-rw-r--r--pretyping/reductionops.ml21
-rw-r--r--pretyping/reductionops.mli7
-rw-r--r--pretyping/tacred.ml5
-rw-r--r--tactics/cbn.ml12
-rw-r--r--tactics/cbn.mli7
-rw-r--r--tactics/redexpr.ml7
-rw-r--r--tactics/tactics.ml4
-rw-r--r--test-suite/output/Arguments_renaming.out6
-rw-r--r--test-suite/output/Inductive.out2
-rw-r--r--test-suite/output/InitSyntax.out2
-rw-r--r--test-suite/output/PrintInfos.out10
-rw-r--r--test-suite/output/PrintModule.out8
-rw-r--r--test-suite/output/PrintModule.v7
-rw-r--r--test-suite/output/UnivBinders.out16
-rw-r--r--theories/Numbers/HexadecimalNat.v2
-rw-r--r--vernac/printmod.ml4
17 files changed, 67 insertions, 59 deletions
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index 8873d02888..8c8c88c526 100644
--- a/doc/sphinx/proofs/writing-proofs/rewriting.rst
+++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst
@@ -890,10 +890,8 @@ the conversion in hypotheses :n:`{+ @ident}`.
Conversion tactics applied to hypotheses
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-.. tacn:: @tactic in {+, @ident}
-
- Applies :token:`tactic` (any of the conversion tactics listed in this
- section) to the hypotheses :n:`{+ @ident}`.
+ The form :n:`@tactic in {+, @ident }` applies :token:`tactic` (any of the
+ conversion tactics listed in this section) to the hypotheses :n:`{+ @ident}`.
If :token:`ident` is a local definition, then :token:`ident` can be replaced by
:n:`type of @ident` to address not the body but the type of the local
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 10caf855ba..54a47a252d 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -468,23 +468,6 @@ let safe_meta_value sigma ev =
try Some (Evd.meta_value sigma ev)
with Not_found -> None
-let strong_with_flags whdfun flags env sigma t =
- let push_rel_check_zeta d env =
- let open CClosure.RedFlags in
- let d = match d with
- | LocalDef (na,c,t) when not (red_set flags fZETA) -> LocalAssum (na,t)
- | d -> d in
- push_rel d env in
- let rec strongrec env t =
- map_constr_with_full_binders env sigma
- push_rel_check_zeta strongrec env (whdfun flags env sigma t) in
- strongrec env t
-
-let strong whdfun env sigma t =
- let rec strongrec env t =
- map_constr_with_full_binders env sigma push_rel strongrec env (whdfun env sigma t) in
- strongrec env t
-
(*************************************)
(*** Reduction using bindingss ***)
(*************************************)
@@ -1284,7 +1267,9 @@ let plain_instance sigma s c = match s with
let instance env sigma s c =
(* if s = [] then c else *)
- strong whd_betaiota env sigma (plain_instance sigma s c)
+ (* No need to compute contexts under binders as whd_betaiota is local *)
+ let rec strongrec t = EConstr.map sigma strongrec (whd_betaiota env sigma t) in
+ strongrec (plain_instance sigma s c)
(* pseudo-reduction rule:
* [hnf_prod_app env s (Prod(_,B)) N --> B[N]
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 9d41e7ab58..41d16f1c3c 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -143,13 +143,6 @@ type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
type stack_reduction_function =
env -> evar_map -> constr -> constr * constr list
-(** {6 Reduction Function Operators } *)
-
-val strong_with_flags :
- (CClosure.RedFlags.reds -> reduction_function) ->
- (CClosure.RedFlags.reds -> reduction_function)
-val strong : reduction_function -> reduction_function
-
(** {6 Generic Optimized Reduction Function using Closures } *)
val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 1523ec502d..a103699716 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1054,7 +1054,10 @@ let hnf_constr env sigma c = whd_simpl_orelse_delta_but_fix env sigma (c, [])
let whd_simpl env sigma c =
applist (whd_simpl_stack env sigma (c, []))
-let simpl env sigma c = strong whd_simpl env sigma c
+let simpl env sigma c =
+ let rec strongrec env t =
+ map_constr_with_full_binders env sigma push_rel strongrec env (whd_simpl env sigma t) in
+ strongrec env c
(* Reduction at specific subterms *)
diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index 39959d6fb8..6fb6cff04f 100644
--- a/tactics/cbn.ml
+++ b/tactics/cbn.ml
@@ -820,3 +820,15 @@ let whd_cbn flags env sigma t =
(whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t, Stack.empty))
in
Stack.zip ~refold:true sigma state
+
+let norm_cbn flags env sigma t =
+ let push_rel_check_zeta d env =
+ let open CClosure.RedFlags in
+ let d = match d with
+ | LocalDef (na,c,t) when not (red_set flags fZETA) -> LocalAssum (na,t)
+ | d -> d in
+ push_rel d env in
+ let rec strongrec env t =
+ map_constr_with_full_binders env sigma
+ push_rel_check_zeta strongrec env (whd_cbn flags env sigma t) in
+ strongrec env t
diff --git a/tactics/cbn.mli b/tactics/cbn.mli
index af54771382..a02a74f9e4 100644
--- a/tactics/cbn.mli
+++ b/tactics/cbn.mli
@@ -8,6 +8,13 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+(** Weak-head cbn reduction. Despite the name, the cbn reduction is a complex
+ reduction distinct from call-by-name or call-by-need. *)
val whd_cbn :
CClosure.RedFlags.reds ->
Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr
+
+(** Strong variant of cbn reduction. *)
+val norm_cbn :
+ CClosure.RedFlags.reds ->
+ Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
index b415b30de8..87cae3abe5 100644
--- a/tactics/redexpr.ml
+++ b/tactics/redexpr.ml
@@ -46,9 +46,6 @@ let cbv_native env sigma c =
let whd_cbn = Cbn.whd_cbn
-let strong_cbn flags =
- strong_with_flags whd_cbn flags
-
let simplIsCbn =
Goptions.declare_bool_option_and_ref ~depr:false ~key:["SimplIsCbn"] ~value:false
@@ -248,11 +245,11 @@ let reduction_of_red_expr_val = function
| Hnf -> (e_red hnf_constr,DEFAULTcast)
| Simpl (f,o) ->
let whd_am = if simplIsCbn () then whd_cbn f else whd_simpl in
- let am = if simplIsCbn () then strong_cbn f else simpl in
+ let am = if simplIsCbn () then Cbn.norm_cbn f else simpl in
(contextualize (if head_style then whd_am else am) am o,DEFAULTcast)
| Cbv f -> (e_red (cbv_norm_flags f),DEFAULTcast)
| Cbn f ->
- (e_red (strong_cbn f), DEFAULTcast)
+ (e_red (Cbn.norm_cbn f), DEFAULTcast)
| Lazy f -> (e_red (clos_norm_flags f),DEFAULTcast)
| Unfold ubinds -> (e_red (unfoldn (List.map out_with_occurrences ubinds)),DEFAULTcast)
| Fold cl -> (e_red (fold_commands cl),DEFAULTcast)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f72764945c..c64f583428 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1244,8 +1244,6 @@ let force_destruction_arg with_evars env sigma c =
(* tactic "cut" (actually modus ponens) *)
(****************************************)
-let normalize_cut = false
-
let cut c =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
@@ -1260,8 +1258,6 @@ let cut c =
| sigma, s ->
let r = Sorts.relevance_of_sort s in
let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in
- (* Backward compat: normalize [c]. *)
- let c = if normalize_cut then strong whd_betaiota env sigma c else c in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(Refine.refine ~typecheck:false begin fun h ->
let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c r (Vars.lift 1 concl)) in
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index e46774f68a..9fd846ac16 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -11,7 +11,7 @@ eq_refl
: ?y = ?y
where
?y : [ |- nat]
-Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x
+Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x.
Arguments eq {A}%type_scope _ _
Arguments eq_refl {B}%type_scope {y}, [_] _
@@ -22,7 +22,7 @@ eq_refl is not universe polymorphic
Arguments eq_refl {B}%type_scope {y}, [_] _
(where some original arguments have been renamed)
Expands to: Constructor Coq.Init.Logic.eq_refl
-Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x
+Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x.
Arguments myEq _%type_scope _ _
Arguments myrefl {C}%type_scope x _
@@ -55,7 +55,7 @@ Expands to: Constant Arguments_renaming.Test1.myplus
@myplus
: forall Z : Type, Z -> nat -> nat -> nat
Inductive myEq (A B : Type) (x : A) : A -> Prop :=
- myrefl : B -> myEq A B x x
+ myrefl : B -> myEq A B x x.
Arguments myEq (_ _)%type_scope _ _
Arguments myrefl A%type_scope {C}%type_scope x _
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
index 8e10107673..fc3b6fbd99 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -5,7 +5,7 @@ A : Set
a : A
l : list' A
Unable to unify "list' (A * A)%type" with "list' A".
-Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x
+Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x.
Arguments foo _%type_scope _
Arguments Foo _%type_scope _
diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out
index 02e58775b5..fdd609f5b2 100644
--- a/test-suite/output/InitSyntax.out
+++ b/test-suite/output/InitSyntax.out
@@ -1,5 +1,5 @@
Inductive sig2 (A : Type) (P Q : A -> Prop) : Type :=
- exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x}
+ exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x}.
Arguments sig2 [A]%type_scope (_ _)%type_scope
Arguments exist2 [A]%type_scope (_ _)%function_scope _ _ _
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index fe16dba496..03b9e3b527 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -4,14 +4,14 @@ existT is template universe polymorphic on sigT.u0 sigT.u1
Arguments existT [A]%type_scope _%function_scope _ _
Expands to: Constructor Coq.Init.Specif.existT
Inductive sigT (A : Type) (P : A -> Type) : Type :=
- existT : forall x : A, P x -> {x : A & P x}
+ existT : forall x : A, P x -> {x : A & P x}.
Arguments sigT [A]%type_scope _%type_scope
Arguments existT [A]%type_scope _%function_scope _ _
existT : forall [A : Type] (P : A -> Type) (x : A), P x -> {x : A & P x}
Argument A is implicit
-Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x
+Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x.
Arguments eq {A}%type_scope _ _
Arguments eq_refl {A}%type_scope {x}, [_] _
@@ -50,7 +50,7 @@ Arguments plus_n_O _%nat_scope
plus_n_O is opaque
Expands to: Constant Coq.Init.Peano.plus_n_O
Inductive le (n : nat) : nat -> Prop :=
- le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m
+ le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m.
Arguments le (_ _)%nat_scope
Arguments le_n _%nat_scope
@@ -60,7 +60,7 @@ comparison : Set
comparison is not universe polymorphic
Expands to: Inductive Coq.Init.Datatypes.comparison
Inductive comparison : Set :=
- Eq : comparison | Lt : comparison | Gt : comparison
+ Eq : comparison | Lt : comparison | Gt : comparison.
bar : foo
bar is not universe polymorphic
@@ -78,7 +78,7 @@ Arguments bar {x}
Module Coq.Init.Peano
Notation sym_eq := eq_sym
Expands to: Notation Coq.Init.Logic.sym_eq
-Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x
+Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x.
Arguments eq {A}%type_scope _ _
Arguments eq_refl {A}%type_scope {x}, {_} _
diff --git a/test-suite/output/PrintModule.out b/test-suite/output/PrintModule.out
index 1a9bc068c5..7c7600b786 100644
--- a/test-suite/output/PrintModule.out
+++ b/test-suite/output/PrintModule.out
@@ -7,3 +7,11 @@ Module N : S with Module T := K := M
Module N : S with Module T := M
Module Type Func = Funsig (T0:Test) Sig Parameter x : T0.t. End
+Module
+A
+:= Struct
+ Variant I : Set := C : nat -> I.
+ Record R : Set := Build_R { n : nat }.
+ Definition n : R -> nat.
+ End
+
diff --git a/test-suite/output/PrintModule.v b/test-suite/output/PrintModule.v
index 54ef305be4..b4de03b556 100644
--- a/test-suite/output/PrintModule.v
+++ b/test-suite/output/PrintModule.v
@@ -60,3 +60,10 @@ Print Func.
End Shortest_path.
End QUX.
+
+Module A.
+Variant I := C : nat -> I.
+Record R := { n : nat }.
+End A.
+
+Print Module A.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 95b6c6ee95..4993b747fa 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -1,6 +1,7 @@
-Inductive Empty@{uu} : Type@{uu} :=
+Inductive Empty@{uu} : Type@{uu} := .
(* uu |= *)
-Record PWrap (A : Type@{uu}) : Type@{uu} := pwrap { punwrap : A }
+Record PWrap (A : Type@{uu}) : Type@{uu} := pwrap
+ { punwrap : A }.
(* uu |= *)
PWrap has primitive projections with eta conversion.
@@ -12,7 +13,8 @@ fun (A : Type@{uu}) (p : PWrap@{uu} A) => punwrap _ p
(* uu |= *)
Arguments punwrap _%type_scope _
-Record RWrap (A : Type@{uu}) : Type@{uu} := rwrap { runwrap : A }
+Record RWrap (A : Type@{uu}) : Type@{uu} := rwrap
+ { runwrap : A }.
(* uu |= *)
Arguments RWrap _%type_scope
@@ -80,9 +82,9 @@ foo@{uu u v} =
Type@{u} -> Type@{v} -> Type@{uu}
: Type@{max(uu+1,u+1,v+1)}
(* uu u v |= *)
-Inductive Empty@{E} : Type@{E} :=
+Inductive Empty@{E} : Type@{E} := .
(* E |= *)
-Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }
+Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }.
(* E |= *)
PWrap has primitive projections with eta conversion.
@@ -107,7 +109,7 @@ insec@{v} = Type@{uu} -> Type@{v}
: Type@{max(uu+1,v+1)}
(* v |= *)
Inductive insecind@{k} : Type@{k+1} :=
- inseccstr : Type@{k} -> insecind@{k}
+ inseccstr : Type@{k} -> insecind@{k}.
(* k |= *)
Arguments inseccstr _%type_scope
@@ -115,7 +117,7 @@ insec@{uu v} = Type@{uu} -> Type@{v}
: Type@{max(uu+1,v+1)}
(* uu v |= *)
Inductive insecind@{uu k} : Type@{k+1} :=
- inseccstr : Type@{k} -> insecind@{uu k}
+ inseccstr : Type@{k} -> insecind@{uu k}.
(* uu k |= *)
Arguments inseccstr _%type_scope
diff --git a/theories/Numbers/HexadecimalNat.v b/theories/Numbers/HexadecimalNat.v
index 94a14b90bd..696e89bd8e 100644
--- a/theories/Numbers/HexadecimalNat.v
+++ b/theories/Numbers/HexadecimalNat.v
@@ -230,7 +230,7 @@ Proof.
simpl_of_lu;
rewrite ?Nat.add_succ_l, Nat.add_0_l, ?to_lu_succ, to_of_lu_sixteenfold
by assumption;
- unfold lnorm; simpl; now destruct nztail.
+ unfold lnorm; cbn; now destruct nztail.
Qed.
(** Second bijection result *)
diff --git a/vernac/printmod.ml b/vernac/printmod.ml
index fdf7f6c74a..ba4a7857e7 100644
--- a/vernac/printmod.ml
+++ b/vernac/printmod.ml
@@ -124,7 +124,7 @@ let print_mutual_inductive env mind mib udecl =
let sigma = Evd.from_ctx (UState.of_binders bl) in
hov 0 (def keyword ++ spc () ++
prlist_with_sep (fun () -> fnl () ++ str" with ")
- (print_one_inductive env sigma mib) inds ++
+ (print_one_inductive env sigma mib) inds ++ str "." ++
Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes)
let get_fields =
@@ -173,7 +173,7 @@ let print_record env mind mib udecl =
prlist_with_sep (fun () -> str ";" ++ brk(2,0))
(fun (id,b,c) ->
Id.print id ++ str (if b then " : " else " := ") ++
- Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++
+ Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }." ++
Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes
)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 10:41:12 +0000