diff options
| author | Emilio Jesus Gallego Arias | 2020-06-24 16:27:03 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-26 14:38:14 +0200 |
| commit | eb950dffbc1729c984cb52d9a876a64e8f40db4c (patch) | |
| tree | 220bc120d1c3c2279e8fb09de6f541b7c68ba7ec | |
| parent | a5a65ddcf0e476384c827cdf2445bc554eae825a (diff) | |
[recLemmas] Nit on naming consistency.
| -rw-r--r-- | vernac/recLemmas.ml | 6 | ||||
| -rw-r--r-- | vernac/recLemmas.mli | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 6 |
3 files changed, 7 insertions, 7 deletions
diff --git a/vernac/recLemmas.ml b/vernac/recLemmas.ml index e276918526..534c358a3f 100644 --- a/vernac/recLemmas.ml +++ b/vernac/recLemmas.ml @@ -93,7 +93,7 @@ type mutual_info = | NonMutual of EConstr.t Declare.CInfo.t | Mutual of { mutual_info : Declare.Proof.mutual_info - ; thms : EConstr.t Declare.CInfo.t list + ; cinfo : EConstr.t Declare.CInfo.t list ; possible_guards : int list } @@ -106,6 +106,6 @@ let look_for_possibly_mutual_statements sigma thms : mutual_info = (* More than one statement and/or an explicit decreasing mark: *) (* we look for a common inductive hyp or a common coinductive conclusion *) let recguard,ordered_inds = find_mutually_recursive_statements sigma thms in - let thms = List.map pi2 ordered_inds in - Mutual { mutual_info = recguard; thms; possible_guards = List.map (fun (_,_,i) -> succ i) ordered_inds } + let cinfo = List.map pi2 ordered_inds in + Mutual { mutual_info = recguard; cinfo; possible_guards = List.map (fun (_,_,i) -> succ i) ordered_inds } | [] -> CErrors.anomaly (Pp.str "Empty list of theorems.") diff --git a/vernac/recLemmas.mli b/vernac/recLemmas.mli index a1cadd9bc1..93aae29b18 100644 --- a/vernac/recLemmas.mli +++ b/vernac/recLemmas.mli @@ -12,7 +12,7 @@ type mutual_info = | NonMutual of EConstr.t Declare.CInfo.t | Mutual of { mutual_info : Declare.Proof.mutual_info - ; thms : EConstr.t Declare.CInfo.t list + ; cinfo : EConstr.t Declare.CInfo.t list ; possible_guards : int list } diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index cc582727e3..d44e4babf4 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -533,11 +533,11 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms = let evd = post_check_evd ~udecl ~poly evd in let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in Declare.Proof.start_with_initialization ~info ~cinfo:thm evd - | RecLemmas.Mutual { mutual_info; thms ; possible_guards } -> - let thms = List.map (Declare.CInfo.to_constr evd) thms in + | RecLemmas.Mutual { mutual_info; cinfo ; possible_guards } -> + let cinfo = List.map (Declare.CInfo.to_constr evd) cinfo in let evd = post_check_evd ~udecl ~poly evd in let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in - Declare.Proof.start_mutual_with_initialization ~info ~cinfo:thms evd ~mutual_info (Some possible_guards) + Declare.Proof.start_mutual_with_initialization ~info ~cinfo evd ~mutual_info (Some possible_guards) let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in function | Coercion -> |