aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-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
5 files changed, 27 insertions, 42 deletions
diff --git a/vernac/command.ml b/vernac/command.ml
index b27d8a0a3..3ea8f6590 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 7cd0afeec..9bbc2fdac 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 993a2c260..1344701ff 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 681413a29..d06b8fd14 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 0a5a000fe..2cb6f3918 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.39.1) at 2024-06-17 17:35:40 +0000