aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/refman/RefMan-tac.tex6
-rw-r--r--ide/texmacspp.ml2
-rw-r--r--interp/topconstr.ml7
-rw-r--r--intf/constrexpr.mli2
-rw-r--r--intf/vernacexpr.mli2
-rw-r--r--kernel/constr.ml9
-rw-r--r--parsing/g_vernac.ml44
-rw-r--r--printing/ppvernac.ml3
-rw-r--r--tactics/tactics.ml3
-rw-r--r--test-suite/success/ImplicitArguments.v6
-rw-r--r--vernac/command.ml24
-rw-r--r--vernac/command.mli8
-rw-r--r--vernac/lemmas.ml29
-rw-r--r--vernac/lemmas.mli4
-rw-r--r--vernac/vernacentries.ml4
15 files changed, 60 insertions, 53 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 3f12411863..0edc66f839 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2618,9 +2618,9 @@ as the ones described in Section~\ref{Tac-induction}.
In the syntax of the tactic, the identifier {\ident} is the name given
to the induction hypothesis. The natural number {\num} tells on which
premise of the current goal the induction acts, starting
-from 1 and counting both dependent and non dependent
-products. Especially, the current lemma must be composed of at least
-{\num} products.
+from 1, counting both dependent and non dependent
+products, but skipping local definitions. Especially, the current
+lemma must be composed of at least {\num} products.
Like in a {\tt fix} expression, the induction
hypotheses have to be used on structurally smaller arguments.
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index e20704b7fb..05f1820cf2 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -552,7 +552,7 @@ let rec tmpp v loc =
let str_dk = Kindops.string_of_definition_kind (l, false, dk) in
let str_id = Id.to_string id in
(xmlDef str_dk str_id loc [pp_expr e])
- | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) ->
+ | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement) ], b) ->
let str_tk = Kindops.string_of_theorem_kind tk in
let str_id = Id.to_string id in
(xmlThm str_tk str_id loc [pp_expr statement])
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index d3142e7f0c..e05be65fb0 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -178,7 +178,12 @@ let split_at_annot bl na =
in
(List.rev ans, CLocalAssum (r, k, t) :: rest)
end
- | CLocalDef _ as x :: rest -> aux (x :: acc) rest
+ | CLocalDef ((_,na),_,_) as x :: rest ->
+ if Name.equal (Name id) na then
+ user_err ~loc
+ (Nameops.pr_id id ++ str" must be a proper parameter and not a local definition.")
+ else
+ aux (x :: acc) rest
| CLocalPattern (loc,_,_) :: rest ->
Loc.raise ~loc (Stream.Error "pattern with quote not allowed after fix")
| [] ->
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index 49bafadc8e..a4a6eb9092 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -19,7 +19,7 @@ open Decl_kinds
type notation = string
type explicitation =
- | ExplByPos of int * Id.t option
+ | ExplByPos of int * Id.t option (* a reference to the n-th product starting from left *)
| ExplByName of Id.t
type binder_kind =
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index f018d59e6b..cb093d85d5 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -209,7 +209,7 @@ type one_inductive_expr =
plident * local_binder_expr list * constr_expr option * constructor_expr list
type proof_expr =
- plident option * (local_binder_expr list * constr_expr * (lident option * recursion_order_expr) option)
+ plident option * (local_binder_expr list * constr_expr)
type syntax_modifier =
| SetItemLevel of string list * Extend.production_level
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 5a7561bf50..e2630c3f08 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -107,7 +107,16 @@ type constr = t
type existential = existential_key * constr array
type rec_declaration = Name.t array * constr array * constr array
type fixpoint = (int array * int) * rec_declaration
+ (* The array of [int]'s tells for each component of the array of
+ mutual fixpoints the number of lambdas to skip before finding the
+ recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B)
+ (v:=u) (w:I) {struct w}"), telling to skip x and z and that w is
+ the recursive argument);
+ The second component [int] tells which component of the block is
+ returned *)
type cofixpoint = int * rec_declaration
+ (* The component [int] tells which component of the block of
+ cofixpoint is returned *)
type types = constr
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 011565d86a..8f6b28f130 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -136,8 +136,8 @@ GEXTEND Gram
[ [ thm = thm_token; id = pidentref; bl = binders; ":"; c = lconstr;
l = LIST0
[ "with"; id = pidentref; bl = binders; ":"; c = lconstr ->
- (Some id,(bl,c,None)) ] ->
- VernacStartTheoremProof (thm, (Some id,(bl,c,None))::l, false)
+ (Some id,(bl,c)) ] ->
+ VernacStartTheoremProof (thm, (Some id,(bl,c))::l, false)
| stre = assumption_token; nl = inline; bl = assum_list ->
VernacAssumption (stre, nl, bl)
| (kwd,stre) = assumptions_token; nl = inline; bl = assum_list ->
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index e4a87739b1..f0c8cd58c1 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -386,13 +386,12 @@ open Decl_kinds
++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr def) def
++ prlist (pr_decl_notation pr_constr) ntn
- let pr_statement head (idpl,(bl,c,guard)) =
+ let pr_statement head (idpl,(bl,c)) =
assert (not (Option.is_empty idpl));
let id, pl = Option.get idpl in
hov 2
(head ++ spc() ++ pr_lident id ++ pr_univs pl ++ spc() ++
(match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
- pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++
str":" ++ pr_spc_lconstr c)
let pr_priority = function
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 9c2a1d8509..4173f87340 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -512,6 +512,9 @@ let rec check_mutind env sigma k cl = match EConstr.kind sigma (strip_outer_cast
else
let open Context.Rel.Declaration in
check_mutind (push_rel (LocalAssum (na, c1)) env) sigma (pred k) b
+| LetIn (na, c1, t, b) ->
+ let open Context.Rel.Declaration in
+ check_mutind (push_rel (LocalDef (na, c1, t)) env) sigma k b
| _ -> error "Not enough products."
(* Refine as a fixpoint *)
diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index f702aa62f1..f07773f8bd 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -21,3 +21,9 @@ Fixpoint app {A : Type} {n m : nat} (v : vector A n) (w : vector A m) : vector A
(* Test sharing information between different hypotheses *)
Parameters (a:_) (b:a=0).
+
+(* These examples were failing due to a lifting wrongly taking let-in into account *)
+
+Definition foo6 (x:=1) : forall {n:nat}, n=n := fun n => eq_refl.
+
+Fixpoint foo7 (x:=1) (n:nat) {p:nat} {struct n} : nat.
diff --git a/vernac/command.ml b/vernac/command.ml
index b27d8a0a35..3ea8f65906 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -96,7 +96,7 @@ let interp_definition pl bl p red_option c ctypopt =
let evdref = ref (Evd.from_ctx ctx) in
let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in
let ctx = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx in
- let nb_args = List.length ctx in
+ let nb_args = Context.Rel.nhyps ctx in
let imps,pl,ce =
match ctypopt with
None ->
@@ -849,7 +849,7 @@ type structured_fixpoint_expr = {
let interp_fix_context env evdref isfix fix =
let before, after = if isfix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in
let impl_env, ((env', ctx), imps) = interp_context_evars env evdref before in
- let impl_env', ((env'', ctx'), imps') = interp_context_evars ~impl_env ~shift:(List.length before) env' evdref after in
+ let impl_env', ((env'', ctx'), imps') = interp_context_evars ~impl_env ~shift:(Context.Rel.nhyps ctx) env' evdref after in
let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in
((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
@@ -880,8 +880,10 @@ let prepare_recursive_declaration fixnames fixtypes fixdefs =
(* Jump over let-bindings. *)
-let compute_possible_guardness_evidences (ids,_,na) =
- match na with
+let compute_possible_guardness_evidences (ctx,_,recindex) =
+ (* A recursive index is characterized by the number of lambdas to
+ skip before finding the relevant inductive argument *)
+ match recindex with
| Some i -> [i]
| None ->
(* If recursive argument was not given by user, we try all args.
@@ -889,7 +891,7 @@ let compute_possible_guardness_evidences (ids,_,na) =
but doing it properly involves delta-reduction, and it finally
doesn't seem to worth the effort (except for huge mutual
fixpoints ?) *)
- List.interval 0 (List.length ids - 1)
+ List.interval 0 (Context.Rel.nhyps ctx - 1)
type recursive_preentry =
Id.t list * constr option list * types list
@@ -1130,7 +1132,7 @@ let interp_recursive isfix fixl notations =
let fixtypes = List.map2 build_fix_type fixctxs fixccls in
let fixtypes = List.map (fun c -> nf_evar !evdref c) fixtypes in
let fiximps = List.map3
- (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (List.length ctx) cclimps))
+ (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (Context.Rel.nhyps ctx) cclimps))
fixctximps fixcclimps fixctxs in
let rec_sign =
List.fold_left2
@@ -1169,10 +1171,10 @@ let interp_recursive isfix fixl notations =
let fixdefs = List.map (fun c -> Option.map EConstr.Unsafe.to_constr c) fixdefs in
let fixdefs = List.map (Option.map nf) fixdefs in
let fixtypes = List.map nf fixtypes in
- let fixctxnames = List.map (fun (_,ctx) -> List.map RelDecl.get_name ctx) fixctxs in
+ let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in
(* Build the fix declaration block *)
- (env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxnames fiximps fixannots
+ (env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots
let check_recursive isfix env evd (fixnames,fixdefs,_) =
check_evars_are_solved env evd Evd.empty;
@@ -1188,14 +1190,14 @@ let interp_fixpoint l ntns =
let interp_cofixpoint l ntns =
let (env,_,pl,evd),fix,info = interp_recursive false l ntns in
- check_recursive false env evd fix;
+ check_recursive false env evd fix;
(fix,pl,Evd.evar_universe_context evd,info)
let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
if List.exists Option.is_empty fixdefs then
(* Some bodies to define by proof *)
let thms =
- List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps))))
+ List.map3 (fun id t (ctx,imps,_) -> ((id,pl),(t,(List.map RelDecl.get_name ctx,imps))))
fixnames fixtypes fiximps in
let init_tac =
Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
@@ -1229,7 +1231,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
if List.exists Option.is_empty fixdefs then
(* Some bodies to define by proof *)
let thms =
- List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps))))
+ List.map3 (fun id t (ctx,imps,_) -> ((id,pl),(t,(List.map RelDecl.get_name ctx,imps))))
fixnames fixtypes fiximps in
let init_tac =
Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
diff --git a/vernac/command.mli b/vernac/command.mli
index 7cd0afeec3..9bbc2fdac1 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -138,24 +138,24 @@ type recursive_preentry =
val interp_fixpoint :
structured_fixpoint_expr list -> decl_notation list ->
recursive_preentry * lident list option * Evd.evar_universe_context *
- (Name.t list * Impargs.manual_implicits * int option) list
+ (EConstr.rel_context * Impargs.manual_implicits * int option) list
val interp_cofixpoint :
structured_fixpoint_expr list -> decl_notation list ->
recursive_preentry * lident list option * Evd.evar_universe_context *
- (Name.t list * Impargs.manual_implicits * int option) list
+ (EConstr.rel_context * Impargs.manual_implicits * int option) list
(** Registering fixpoints and cofixpoints in the environment *)
val declare_fixpoint :
locality -> polymorphic ->
recursive_preentry * lident list option * Evd.evar_universe_context *
- (Name.t list * Impargs.manual_implicits * int option) list ->
+ (Context.Rel.t * Impargs.manual_implicits * int option) list ->
lemma_possible_guards -> decl_notation list -> unit
val declare_cofixpoint : locality -> polymorphic ->
recursive_preentry * lident list option * Evd.evar_universe_context *
- (Name.t list * Impargs.manual_implicits * int option) list ->
+ (Context.Rel.t * Impargs.manual_implicits * int option) list ->
decl_notation list -> unit
(** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 993a2c260d..1344701ff7 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -88,25 +88,9 @@ let adjust_guardness_conditions const = function
let find_mutually_recursive_statements thms =
let n = List.length thms in
- let inds = List.map (fun (id,(t,impls,annot)) ->
+ let inds = List.map (fun (id,(t,impls)) ->
let (hyps,ccl) = decompose_prod_assum t in
let x = (id,(t,impls)) in
- match annot with
- (* Explicit fixpoint decreasing argument is given *)
- | Some (Some (_,id),CStructRec) ->
- let i,b,typ = lookup_rel_id id hyps in
- (match kind_of_term t with
- | Ind ((kn,_ as ind), u) when
- let mind = Global.lookup_mind kn in
- mind.mind_finite == Decl_kinds.Finite && Option.is_empty b ->
- [ind,x,i],[]
- | _ ->
- error "Decreasing argument is not an inductive assumption.")
- (* Unsupported cases *)
- | Some (_,(CWfRec _|CMeasureRec _)) ->
- error "Only structural decreasing is supported for mutual statements."
- (* Cofixpoint or fixpoint w/o explicit decreasing argument *)
- | None | Some (None, CStructRec) ->
let whnf_hyp_hds = map_rel_context_in_env
(fun env c -> EConstr.Unsafe.to_constr (fst (whd_all_stack env Evd.empty (EConstr.of_constr c))))
(Global.env()) hyps in
@@ -116,10 +100,10 @@ let find_mutually_recursive_statements thms =
match kind_of_term t with
| Ind ((kn,_ as ind),u) when
let mind = Global.lookup_mind kn in
- mind.mind_finite <> Decl_kinds.CoFinite && is_local_assum decl ->
+ mind.mind_finite <> Decl_kinds.CoFinite ->
[ind,x,i]
| _ ->
- []) 0 (List.rev whnf_hyp_hds)) in
+ []) 0 (List.rev (List.filter RelDecl.is_local_assum whnf_hyp_hds))) in
let ind_ccl =
let cclenv = push_rel_context hyps (Global.env()) in
let whnf_ccl,_ = whd_all_stack cclenv Evd.empty (EConstr.of_constr ccl) in
@@ -178,7 +162,7 @@ let find_mutually_recursive_statements thms =
(finite,guard,None), ordered_inds
let look_for_possibly_mutual_statements = function
- | [id,(t,impls,None)] ->
+ | [id,(t,impls)] ->
(* One non recursively proved theorem *)
None,[id,(t,impls)],None
| _::_ as thms ->
@@ -458,7 +442,7 @@ let start_proof_com ?inference_hook kind thms hook =
| None -> Evd.from_env env0
| Some l -> Evd.from_ctx (Evd.make_evar_universe_context env0 l))
in
- let thms = List.map (fun (sopt,(bl,t,guard)) ->
+ let thms = List.map (fun (sopt,(bl,t)) ->
let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
let t', imps' = interp_type_evars_impls ~impls env evdref t in
let flags = all_and_fail_flags in
@@ -467,8 +451,7 @@ let start_proof_com ?inference_hook kind thms hook =
let ids = List.map RelDecl.get_name ctx in
(compute_proof_name (pi1 kind) sopt,
(EConstr.Unsafe.to_constr (nf_evar !evdref (EConstr.it_mkProd_or_LetIn t' ctx)),
- (ids, imps @ lift_implicits (List.length ids) imps'),
- guard)))
+ (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps'))))
thms in
let recguard,thms,snl = look_for_possibly_mutual_statements thms in
let evd, nf = Evarutil.nf_evars_and_universes !evdref in
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 681413a297..d06b8fd14b 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -41,8 +41,8 @@ val start_proof_com :
val start_proof_with_initialization :
goal_kind -> Evd.evar_map ->
(bool * lemma_possible_guards * unit Proofview.tactic list option) option ->
- ((Id.t * universe_binders option) *
- (types * (Name.t list * Impargs.manual_explicitation list))) list
+ ((Id.t (* name of thm *) * universe_binders option) *
+ (types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
-> int list option -> unit declaration_hook -> unit
val universe_proof_terminator :
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 0a5a000fec..2cb6f3918f 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -477,7 +477,7 @@ let vernac_definition locality p (local,k) ((loc,id as lid),pl) def =
(match def with
| ProveBody (bl,t) -> (* local binders, typ *)
start_proof_and_print (local,p,DefinitionBody k)
- [Some (lid,pl), (bl,t,None)] hook
+ [Some (lid,pl), (bl,t)] hook
| DefineBody (bl,red_option,c,typ_opt) ->
let red_option = match red_option with
| None -> None
@@ -2055,7 +2055,7 @@ let interp ?proof ~loc locality poly c =
| VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n")
(* Proof management *)
- | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t,None)] false
+ | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t)] false
| VernacFocus n -> vernac_focus n
| VernacUnfocus -> vernac_unfocus ()
| VernacUnfocused -> vernac_unfocused ()
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 03:33:16 +0000