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

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

2 files changed, 13 insertions, 0 deletions

diff --git a/kernel/vars.ml b/kernel/vars.ml
index b27e27fda..4affb5f9f 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -181,6 +181,15 @@ let subst_of_rel_context_instance sign l =
 let adjust_subst_to_rel_context sign l =
   List.rev (subst_of_rel_context_instance sign l)
 
+let adjust_rel_to_rel_context sign n =
+  let rec aux sign =
+    let open RelDecl in
+    match sign with
+    | LocalAssum _ :: sign' -> let (n',p) = aux sign' in (n'+1,p)
+    | LocalDef (_,c,_)::sign' -> let (n',p) = aux sign' in (n'+1,if n'<n then p+1 else p)
+    | [] -> (0,n)
+  in snd (aux sign)
+
 (* (thin_val sigma) removes identity substitutions from sigma *)
 
 let rec thin_val = function
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