From f5575393258492837d3764d07f8290b576f61160 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 22 Dec 2016 21:32:35 +0100 Subject: Fixing injection in the presence of let-in in constructors. This also fixes decide equality, discriminate, ... (see e.g. #5279). --- kernel/vars.ml | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'kernel/vars.ml') diff --git a/kernel/vars.ml b/kernel/vars.ml index b27e27fdac..4affb5f9fb 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' (0,n) + in snd (aux sign) + (* (thin_val sigma) removes identity substitutions from sigma *) let rec thin_val = function -- cgit v1.2.3