Fixing injection in the presence of let-in in constructors.

This also fixes decide equality, discriminate, ... (see e.g. #5279).

1 files changed, 4 insertions, 0 deletions

diff --git a/kernel/vars.mli b/kernel/vars.mli
index 574d50ecc..f7535e6d8 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -73,6 +73,10 @@ val subst_of_rel_context_instance : Context.Rel.t -> constr list -> substl
 (** For compatibility: returns the substitution reversed *)
 val adjust_subst_to_rel_context : Context.Rel.t -> constr list -> constr list
 
+(** Take an index in an instance of a context and returns its index wrt to
+    the full context (e.g. 2 in [x:A;y:=b;z:C] is 3, i.e. a reference to z) *)
+val adjust_rel_to_rel_context : Context.Rel.t -> int -> int
+
 (** [substnl [a₁;...;an] k c] substitutes in parallel [a₁],...,[an]
     for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates
     accordingly indexes in [an],...,[a1] and [c]. In terms of typing, if