From 17a5e95cd38206d82a1ff83c1d155a9a26729495 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 28 Apr 2020 16:43:10 +0200
Subject: Add comment about decide equality dependence computation.

---
 vernac/auto_ind_decl.ml | 5 +++++
 1 file changed, 5 insertions(+)

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
-- 
cgit v1.2.3