aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES2
-rw-r--r--doc/refman/RefMan-tac.tex32
-rw-r--r--grammar/q_coqast.ml415
-rw-r--r--interp/smartlocate.ml4
-rw-r--r--interp/smartlocate.mli2
-rw-r--r--intf/genredexpr.mli6
-rw-r--r--parsing/g_tactic.ml418
-rw-r--r--pretyping/miscops.ml25
-rw-r--r--pretyping/miscops.mli6
-rw-r--r--printing/ppconstr.ml10
-rw-r--r--proofs/redexpr.ml66
-rw-r--r--tactics/tacintern.ml23
-rw-r--r--tactics/tacinterp.ml6
-rw-r--r--tactics/tacsubst.ml16
-rw-r--r--test-suite/success/simpl.v34
-rw-r--r--theories/Numbers/Cyclic/Abstract/CyclicAxioms.v2
16 files changed, 176 insertions, 91 deletions
diff --git a/CHANGES b/CHANGES
index 8aa42bb63..f75085a83 100644
--- a/CHANGES
+++ b/CHANGES
@@ -156,6 +156,8 @@ Tactics
- "change ... in ..." and "simpl ... in ..." now consider nested
occurrences (possible source of incompatibilities since this alters
the numbering of occurrences).
+- simpl, vm_compute and native_compute can be given a notation string to a
+ constant as argument.
- The "change p with c" tactic semantics changed, now type-checking
"c" at each matching occurrence "t" of the pattern "p", and
converting "t" with "c".
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 75ba90f03..5c87b12cc 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3080,16 +3080,17 @@ The term \verb+forall n:nat, (plus (S n) (S n))+ is not reduced by {\tt hnf}.
These tactics apply to any goal. They try to reduce a term to
something still readable instead of fully normalizing it. They perform
-a sort of strong normalisation with two key differences:
+a sort of strong normalization with two key differences:
\begin{itemize}
-\item They unfold a constant if and only if it leads to an
- $\iota$-reduction, i.e. reducing a match or unfold a fixpoint.
-\item While reducing (co)fixpoints, the tactics use the name of the
+\item They unfold a constant if and only if it leads to a
+ $\iota$-reduction, i.e. reducing a match or unfolding a fixpoint.
+\item While reducing a constant unfolding to (co)fixpoints,
+ the tactics use the name of the
constant the (co)fixpoint comes from instead of the (co)fixpoint
definition in recursive calls.
\end{itemize}
-The \texttt{cbn} tactic claims to be a more principled, faster and more
+The \texttt{cbn} tactic is claimed to be a more principled, faster and more
predictable replacement for \texttt{simpl}.
The \texttt{cbn} tactic accepts the same flags as \texttt{cbv} and
@@ -3169,27 +3170,32 @@ reduced to \texttt{S t}.
[\qualid$_1$\ldots\qualid$_k$] iota zeta} and {\tt cbn beta delta
-[\qualid$_1$\ldots\qualid$_k$] iota zeta} (see \ref{vmcompute}).
-\item {\tt simpl {\term}}
+\item {\tt simpl {\pattern}}
- This applies {\tt simpl} only to the occurrences of {\term} in the
+ This applies {\tt simpl} only to the subterms matching {\pattern} in the
current goal.
-\item {\tt simpl {\term} at \num$_1$ \dots\ \num$_i$}
+\item {\tt simpl {\pattern} at \num$_1$ \dots\ \num$_i$}
This applies {\tt simpl} only to the \num$_1$, \dots, \num$_i$
- occurrences of {\term} in the current goal.
+ occurrences of the subterms matching {\pattern} in the current goal.
\ErrMsg {\tt Too few occurrences}
-\item {\tt simpl {\ident}}
+\item {\tt simpl {\qualid}}\\
+ {\tt simpl {\qstring}}
This applies {\tt simpl} only to the applicative subterms whose head
- occurrence is {\ident}.
+ occurrence is the unfoldable constant {\qualid} (the constant can be
+ referred to by its notation using {\qstring} if such a notation
+ exists).
-\item {\tt simpl {\ident} at \num$_1$ \dots\ \num$_i$}
+\item {\tt simpl {\qualid} at \num$_1$ \dots\ \num$_i$}\\
+ {\tt simpl {\qstring} at \num$_1$ \dots\ \num$_i$}\\
This applies {\tt simpl} only to the \num$_1$, \dots, \num$_i$
-applicative subterms whose head occurrence is {\ident}.
+ applicative subterms whose head occurrence is {\qualid} (or
+ {\qstring}).
\end{Variants}
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 02becc496..d6d13375e 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -46,6 +46,10 @@ let mlexpr_of_reference = function
| Libnames.Ident (loc,id) ->
let loc = of_coqloc loc in <:expr< Libnames.Ident $dloc$ $mlexpr_of_ident id$ >>
+let mlexpr_of_union f g = function
+ | Util.Inl a -> <:expr< Util.Inl $f a$ >>
+ | Util.Inr b -> <:expr< Util.Inr $g b$ >>
+
let mlexpr_of_located f (loc,x) =
let loc = of_coqloc loc in
<:expr< ($dloc$, $f x$) >>
@@ -184,10 +188,15 @@ let rec mlexpr_of_constr = function
let mlexpr_of_occ_constr =
mlexpr_of_occurrences mlexpr_of_constr
+let mlexpr_of_occ_ref_or_constr =
+ mlexpr_of_occurrences
+ (mlexpr_of_union
+ (mlexpr_of_by_notation mlexpr_of_reference) mlexpr_of_constr)
+
let mlexpr_of_red_expr = function
| Genredexpr.Red b -> <:expr< Genredexpr.Red $mlexpr_of_bool b$ >>
| Genredexpr.Hnf -> <:expr< Genredexpr.Hnf >>
- | Genredexpr.Simpl o -> <:expr< Genredexpr.Simpl $mlexpr_of_option mlexpr_of_occ_constr o$ >>
+ | Genredexpr.Simpl o -> <:expr< Genredexpr.Simpl $mlexpr_of_option mlexpr_of_occ_ref_or_constr o$ >>
| Genredexpr.Cbv f ->
<:expr< Genredexpr.Cbv $mlexpr_of_red_flags f$ >>
| Genredexpr.Cbn f ->
@@ -203,8 +212,8 @@ let mlexpr_of_red_expr = function
| Genredexpr.Pattern l ->
let f = mlexpr_of_list mlexpr_of_occ_constr in
<:expr< Genredexpr.Pattern $f l$ >>
- | Genredexpr.CbvVm o -> <:expr< Genredexpr.CbvVm $mlexpr_of_option mlexpr_of_occ_constr o$ >>
- | Genredexpr.CbvNative o -> <:expr< Genredexpr.CbvNative $mlexpr_of_option mlexpr_of_occ_constr o$ >>
+ | Genredexpr.CbvVm o -> <:expr< Genredexpr.CbvVm $mlexpr_of_option mlexpr_of_occ_ref_or_constr o$ >>
+ | Genredexpr.CbvNative o -> <:expr< Genredexpr.CbvNative $mlexpr_of_option mlexpr_of_occ_ref_or_constr o$ >>
| Genredexpr.ExtraRedExpr s ->
<:expr< Genredexpr.ExtraRedExpr $mlexpr_of_string s$ >>
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 7ad5561e3..422497ab3 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -75,3 +75,7 @@ let smart_global_inductive = function
| ByNotation (loc,ntn,sc) ->
destIndRef
(Notation.interp_notation_as_global_reference loc isIndRef ntn sc)
+
+let loc_of_smart_reference = function
+ | AN r -> loc_of_reference r
+ | ByNotation (loc,_,_) -> loc
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 9006e3687..f8840ca0e 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -37,3 +37,5 @@ val smart_global : ?head:bool -> reference or_by_notation -> global_reference
(** The same for inductive types *)
val smart_global_inductive : reference or_by_notation -> inductive
+(** Return the loc of a smart reference *)
+val loc_of_smart_reference : reference or_by_notation -> Loc.t
diff --git a/intf/genredexpr.mli b/intf/genredexpr.mli
index 1096ecb1f..a59278bb0 100644
--- a/intf/genredexpr.mli
+++ b/intf/genredexpr.mli
@@ -32,7 +32,7 @@ type 'a glob_red_flag = {
type ('a,'b,'c) red_expr_gen =
| Red of bool
| Hnf
- | Simpl of 'c Locus.with_occurrences option
+ | Simpl of ('b,'c) Util.union Locus.with_occurrences option
| Cbv of 'b glob_red_flag
| Cbn of 'b glob_red_flag
| Lazy of 'b glob_red_flag
@@ -40,8 +40,8 @@ type ('a,'b,'c) red_expr_gen =
| Fold of 'a list
| Pattern of 'a Locus.with_occurrences list
| ExtraRedExpr of string
- | CbvVm of 'c Locus.with_occurrences option
- | CbvNative of 'c Locus.with_occurrences option
+ | CbvVm of ('b,'c) Util.union Locus.with_occurrences option
+ | CbvNative of ('b,'c) Util.union Locus.with_occurrences option
type ('a,'b,'c) may_eval =
| ConstrTerm of 'a
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 3b01e988a..324efe53e 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -254,6 +254,12 @@ GEXTEND Gram
pattern_occ:
[ [ c = constr; nl = occs -> (nl,c) ] ]
;
+ ref_or_pattern_occ:
+ (* If a string, it is interpreted as a ref
+ (anyway a Coq string does not reduce) *)
+ [ [ c = smart_global; nl = occs -> nl,Inl c
+ | c = constr; nl = occs -> nl,Inr c ] ]
+ ;
unfold_occ:
[ [ c = smart_global; nl = occs -> (nl,c) ] ]
;
@@ -336,13 +342,13 @@ GEXTEND Gram
red_tactic:
[ [ IDENT "red" -> Red false
| IDENT "hnf" -> Hnf
- | IDENT "simpl"; po = OPT pattern_occ -> Simpl po
+ | IDENT "simpl"; po = OPT ref_or_pattern_occ -> Simpl po
| IDENT "cbv"; s = strategy_flag -> Cbv s
| IDENT "cbn"; s = strategy_flag -> Cbn s
| IDENT "lazy"; s = strategy_flag -> Lazy s
| IDENT "compute"; delta = delta_flag -> Cbv (all_with delta)
- | IDENT "vm_compute"; po = OPT pattern_occ -> CbvVm po
- | IDENT "native_compute"; po = OPT pattern_occ -> CbvNative po
+ | IDENT "vm_compute"; po = OPT ref_or_pattern_occ -> CbvVm po
+ | IDENT "native_compute"; po = OPT ref_or_pattern_occ -> CbvNative po
| IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul
| IDENT "fold"; cl = LIST1 constr -> Fold cl
| IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> Pattern pl ] ]
@@ -351,13 +357,13 @@ GEXTEND Gram
red_expr:
[ [ IDENT "red" -> Red false
| IDENT "hnf" -> Hnf
- | IDENT "simpl"; po = OPT pattern_occ -> Simpl po
+ | IDENT "simpl"; po = OPT ref_or_pattern_occ -> Simpl po
| IDENT "cbv"; s = strategy_flag -> Cbv s
| IDENT "cbn"; s = strategy_flag -> Cbn s
| IDENT "lazy"; s = strategy_flag -> Lazy s
| IDENT "compute"; delta = delta_flag -> Cbv (all_with delta)
- | IDENT "vm_compute"; po = OPT pattern_occ -> CbvVm po
- | IDENT "native_compute"; po = OPT pattern_occ -> CbvNative po
+ | IDENT "vm_compute"; po = OPT ref_or_pattern_occ -> CbvVm po
+ | IDENT "native_compute"; po = OPT ref_or_pattern_occ -> CbvNative po
| IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul
| IDENT "fold"; cl = LIST1 constr -> Fold cl
| IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> Pattern pl
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 83e33f84e..3e5f7577b 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -6,7 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Util
open Misctypes
+open Genredexpr
(** Mapping [cast_type] *)
@@ -36,3 +38,26 @@ let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with
| IntroIdentifier id1, IntroIdentifier id2 -> Names.Id.equal id1 id2
| IntroFresh id1, IntroFresh id2 -> Names.Id.equal id1 id2
| _ -> false
+
+(** Mapping [red_expr_gen] *)
+
+let map_flags f flags =
+ { flags with rConst = List.map f flags.rConst }
+
+let map_occs f (occ,e) = (occ,f e)
+
+let map_union f g = function
+ | Inl a -> Inl (f a)
+ | Inr b -> Inr (g b)
+
+let map_red_expr_gen f g h = function
+ | Fold l -> Fold (List.map f l)
+ | Pattern occs_l -> Pattern (List.map (map_occs f) occs_l)
+ | Simpl occs_o -> Simpl (Option.map (map_occs (map_union g h)) occs_o)
+ | Unfold occs_l -> Unfold (List.map (map_occs g) occs_l)
+ | Cbv flags -> Cbv (map_flags g flags)
+ | Lazy flags -> Lazy (map_flags g flags)
+ | CbvVm occs_o -> CbvVm (Option.map (map_occs (map_union g h)) occs_o)
+ | CbvNative occs_o -> CbvNative (Option.map (map_occs (map_union g h)) occs_o)
+ | Cbn flags -> Cbn (map_flags g flags)
+ | ExtraRedExpr _ | Red _ | Hnf _ as x -> x
diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli
index 6235533d7..eb9b4a780 100644
--- a/pretyping/miscops.mli
+++ b/pretyping/miscops.mli
@@ -7,6 +7,7 @@
(************************************************************************)
open Misctypes
+open Genredexpr
(** Mapping [cast_type] *)
@@ -21,3 +22,8 @@ val glob_sort_eq : glob_sort -> glob_sort -> bool
val intro_pattern_naming_eq :
intro_pattern_naming_expr -> intro_pattern_naming_expr -> bool
+
+(** Mapping [red_expr_gen] *)
+
+val map_red_expr_gen : ('a -> 'd) -> ('b -> 'e) -> ('c -> 'f) ->
+ ('a,'b,'c) red_expr_gen -> ('d,'e,'f) red_expr_gen
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index f90ded281..fd4676530 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -753,10 +753,14 @@ end) = struct
let pr_metaid id = str"?" ++ pr_id id
+ let pr_union pr1 pr2 = function
+ | Inl a -> pr1 a
+ | Inr b -> pr2 b
+
let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function
| Red false -> keyword "red"
| Hnf -> keyword "hnf"
- | Simpl o -> keyword "simpl" ++ pr_opt (pr_with_occurrences pr_pattern) o
+ | Simpl o -> keyword "simpl" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
| Cbv f ->
if f.rBeta && f.rIota && f.rZeta && f.rDelta && List.is_empty f.rConst then
keyword "compute"
@@ -779,9 +783,9 @@ end) = struct
| ExtraRedExpr s ->
str s
| CbvVm o ->
- keyword "vm_compute" ++ pr_opt (pr_with_occurrences pr_pattern) o
+ keyword "vm_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
| CbvNative o ->
- keyword "native_compute" ++ pr_opt (pr_with_occurrences pr_pattern) o
+ keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
let pr_may_eval test prc prlc pr2 pr3 = function
| ConstrEval (r,c) ->
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index acdc52400..fb501c7a5 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -173,19 +173,31 @@ let out_arg = function
let out_with_occurrences (occs,c) =
(Locusops.occurrences_map (List.map out_arg) occs, c)
+let e_red f env evm c = evm, f env evm c
+
+let head_style = false (* Turn to true to have a semantics where simpl
+ only reduce at the head when an evaluable reference is given, e.g.
+ 2+n would just reduce to S(1+n) instead of S(S(n)) *)
+
+let contextualize f g = function
+ | Some (occs,c) ->
+ let l = Locusops.occurrences_map (List.map out_arg) occs in
+ let b,c,h = match c with
+ | Inl r -> true, PRef (global_of_evaluable_reference r),f
+ | Inr c ->
+ let b = if head_style then false else (* compat *) is_reference c in
+ b,c,g in
+ e_red (contextually b (l,c) (fun _ -> h))
+ | None -> e_red g
+
let reduction_of_red_expr env =
let make_flag = make_flag env in
- let e_red f env evm c = evm, f env evm c in
let rec reduction_of_red_expr = function
| Red internal ->
if internal then (e_red try_red_product,DEFAULTcast)
else (e_red red_product,DEFAULTcast)
| Hnf -> (e_red hnf_constr,DEFAULTcast)
- | Simpl (Some (_,c as lp)) ->
- let f = contextually (is_reference c) (out_with_occurrences lp)
- (fun _ -> simpl)
- in (e_red f,DEFAULTcast)
- | Simpl None -> (e_red simpl,DEFAULTcast)
+ | Simpl o -> (contextualize (if head_style then whd_simpl else simpl) simpl o,DEFAULTcast)
| Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast)
| Cbn f ->
let f = strong (fun env evd x -> Stack.zip ~refold:true
@@ -201,50 +213,16 @@ let reduction_of_red_expr env =
(try reduction_of_red_expr (String.Map.find s !red_expr_tab)
with Not_found ->
error("unknown user-defined reduction \""^s^"\"")))
- | CbvVm (Some lp) ->
- let b = is_reference (snd lp) in
- let lp = out_with_occurrences lp in
- let vmfun _ env map c =
- let tpe = Retyping.get_type_of env map c in
- Vnorm.cbv_vm env c tpe
- in
- let redfun = contextually b lp vmfun in
- (e_red redfun, VMcast)
- | CbvVm None -> (e_red cbv_vm, VMcast)
- | CbvNative (Some lp) ->
- let b = is_reference (snd lp) in
- let lp = out_with_occurrences lp in
- let nativefun _ env map c =
- let tpe = Retyping.get_type_of env map c in
- let evars = Nativenorm.evars_of_evar_map map in
- Nativenorm.native_norm env evars c tpe
- in
- let redfun = contextually b lp nativefun in
- (e_red redfun, NATIVEcast)
- | CbvNative None -> (e_red cbv_native, NATIVEcast)
+ | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast)
+ | CbvNative o -> (contextualize cbv_native cbv_native o, VMcast)
in
reduction_of_red_expr
-let subst_flags subs flags =
- { flags with rConst = List.map subs flags.rConst }
-
-let subst_occs subs (occ,e) = (occ,subs e)
-
-let subst_gen_red_expr subs_a subs_b subs_c = function
- | Fold l -> Fold (List.map subs_a l)
- | Pattern occs_l -> Pattern (List.map (subst_occs subs_a) occs_l)
- | Simpl occs_o -> Simpl (Option.map (subst_occs subs_c) occs_o)
- | Unfold occs_l -> Unfold (List.map (subst_occs subs_b) occs_l)
- | Cbv flags -> Cbv (subst_flags subs_b flags)
- | Lazy flags -> Lazy (subst_flags subs_b flags)
- | e -> e
-
-let subst_red_expr subs e =
- subst_gen_red_expr
+let subst_red_expr subs =
+ Miscops.map_red_expr_gen
(Mod_subst.subst_mps subs)
(Mod_subst.subst_evaluable_reference subs)
(Patternops.subst_pattern subs)
- e
let inReduction : bool * string * red_expr -> obj =
declare_object
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index f3c7680b0..0a9182e0b 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -344,8 +344,21 @@ let intern_typed_pattern ist p =
(* type it, so we remember the pattern as a glob_constr only *)
(intern_constr_gen true false ist p,dummy_pat)
-let intern_typed_pattern_with_occurrences ist (l,p) =
- (l,intern_typed_pattern ist p)
+let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
+ match p with
+ | Inl r -> l,
+ (try Inl (intern_evaluable ist r)
+ with e when Logic.catchable_exception e ->
+ (* Compatibility. In practice, this means that the code above
+ is useless. Still the idea of having either an evaluable
+ ref or a pattern seems interesting, with "head" reduction
+ in case of an evaluable ref, and "strong" reduction in the
+ subterm matched when a pattern) *)
+ let r = match r with
+ | AN r -> r
+ | _ -> Qualid (loc_of_smart_reference r,qualid_of_path (path_of_global (smart_global r))) in
+ Inr (intern_typed_pattern ist (CRef(r,None))))
+ | Inr c -> l, Inr (intern_typed_pattern ist c)
(* This seems fairly hacky, but it's the first way I've found to get proper
globalization of [unfold]. --adamc *)
@@ -370,9 +383,9 @@ let intern_red_expr ist = function
| Cbn f -> Cbn (intern_flag ist f)
| Lazy f -> Lazy (intern_flag ist f)
| Pattern l -> Pattern (List.map (intern_constr_with_occurrences ist) l)
- | Simpl o -> Simpl (Option.map (intern_typed_pattern_with_occurrences ist) o)
- | CbvVm o -> CbvVm (Option.map (intern_typed_pattern_with_occurrences ist) o)
- | CbvNative o -> CbvNative (Option.map (intern_typed_pattern_with_occurrences ist) o)
+ | Simpl o -> Simpl (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
+ | CbvVm o -> CbvVm (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
+ | CbvNative o -> CbvNative (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
| (Red _ | Hnf | ExtraRedExpr _ as r ) -> r
let intern_in_hyp_as ist lf (clear,id,ipat) =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 54fbbbe27..63eb200de 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -680,8 +680,10 @@ let interp_constr_with_occurrences ist env sigma (occs,c) =
let (sigma,c_interp) = interp_constr ist env sigma c in
sigma , (interp_occurrences ist occs, c_interp)
-let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, c) =
- let _, p = interp_typed_pattern ist env sigma c in
+let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
+ let p = match a with
+ | Inl b -> Inl (interp_evaluable ist env sigma b)
+ | Inr c -> Inr (snd (interp_typed_pattern ist env sigma c)) in
interp_occurrences ist occs, p
let interp_constr_with_occurrences_and_name_as_list =
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 2f47b9000..5a02a53f3 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -114,17 +114,11 @@ let subst_glob_constr_or_pattern subst (c,p) =
let subst_pattern_with_occurrences subst (l,p) =
(l,subst_glob_constr_or_pattern subst p)
-let subst_redexp subst = function
- | Unfold l -> Unfold (List.map (subst_unfold subst) l)
- | Fold l -> Fold (List.map (subst_glob_constr subst) l)
- | Cbv f -> Cbv (subst_flag subst f)
- | Cbn f -> Cbn (subst_flag subst f)
- | Lazy f -> Lazy (subst_flag subst f)
- | Pattern l -> Pattern (List.map (subst_constr_with_occurrences subst) l)
- | Simpl o -> Simpl (Option.map (subst_pattern_with_occurrences subst) o)
- | CbvVm o -> CbvVm (Option.map (subst_pattern_with_occurrences subst) o)
- | CbvNative o -> CbvNative (Option.map (subst_pattern_with_occurrences subst) o)
- | (Red _ | Hnf | ExtraRedExpr _ as r) -> r
+let subst_redexp subst =
+ Miscops.map_red_expr_gen
+ (subst_glob_constr subst)
+ (subst_evaluable subst)
+ (subst_glob_constr_or_pattern subst)
let subst_raw_may_eval subst = function
| ConstrEval (r,c) -> ConstrEval (subst_redexp subst r,subst_glob_constr subst c)
diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v
index 271e6ef76..66a92ea41 100644
--- a/test-suite/success/simpl.v
+++ b/test-suite/success/simpl.v
@@ -45,3 +45,37 @@ Goal forall A B (a:A) l f (i:B), fold_right f i ((a :: l))=i.
simpl.
admit.
Qed. (* Qed will fail if simplification is incorrect (de Bruijn!) *)
+
+(* Check that maximally inserted arguments do not break interpretation
+ of references in simpl, vm_compute etc. *)
+
+Arguments fst {A} {B} p.
+
+Goal fst (0,0) = 0.
+simpl fst.
+Fail set (fst _).
+Abort.
+
+Goal fst (0,0) = 0.
+vm_compute fst.
+Fail set (fst _).
+Abort.
+
+Goal let f x := x + 0 in f 0 = 0.
+intro.
+vm_compute f.
+Fail set (f _).
+Abort.
+
+(* This is a compatibility test with a non evaluable reference, maybe
+ not to be kept for long *)
+Goal 0+0=0.
+simpl @eq.
+Abort.
+
+(* Check reference by notation in simpl *)
+
+Goal 0+0 = 0.
+simpl "+".
+Fail set (_ + _).
+Abort.
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 17c69d226..3586cb7f2 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -290,7 +290,7 @@ Module ZnZ.
intros p Hp.
generalize (spec_of_pos p).
case (of_pos p); intros n w1; simpl.
- case n; simpl Npos; auto with zarith.
+ case n; auto with zarith.
intros p1 Hp1; contradict Hp; apply Z.le_ngt.
replace (base digits) with (1 * base digits + 0) by ring.
rewrite Hp1.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 06:01:31 +0000