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

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

1 files changed, 9 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