From 4ae1fb9619ce2505f0eb6b1f4a4eeed4d8e41489 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 21 Nov 2011 11:41:26 +0000
Subject: Old naming bug in pattern-matching compilation: names in the
 pattern-matching problem generated for the return clause were not the name of
 patterns (no counter-example though, revealed by using generalization more
 intensively).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14709 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/cases.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 99fd7082f2..8694977649 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1522,6 +1522,7 @@ let build_inversion_problem loc env sigma tms t =
 	let pat,acc = make_patvar t acc in
 	let indf' = lift_inductive_family n indf in
 	let sign = make_arity_signature env true indf' in
+	let sign = recover_alias_names alias_of_pat (pat :: List.rev patl) sign in
 	let p = List.length realargs in
 	let env' = push_rels sign env in
 	let patl',acc_sign,acc = aux (n+p+1) env' (sign@acc_sign) tms acc in
-- 
cgit v1.2.3