diff options
| -rw-r--r-- | vernac/auto_ind_decl.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index f8a2d15661..bfa7a729f7 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -133,6 +133,11 @@ let build_beq_scheme_deps kn = let nparrec = mib.mind_nparams_rec in check_no_indices mib; let make_one_eq accu i = + (* This function is only trying to recursively compute the inductive types + appearing as arguments of the constructors. This is done to support + equality decision over hereditarily first-order types. It could be + perfomed in a much cleaner way, e.g. using the kernel normal form of + constructor types and kernel whd_all for the argument types. *) let rec aux accu c = let (c,a) = Reductionops.whd_betaiota_stack Evd.empty EConstr.(of_constr c) in let (c,a) = EConstr.Unsafe.(to_constr c, List.map to_constr a) in |