From 92a5f74259977cc3f92d8b822bdb727a95e64bc6 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 7 Apr 2011 11:04:46 +0000
Subject: Extraction: unfolds the let-in created by Program when handling
 "match"

 This leads to code closer to the original input of the user,
 and moreover some more dummy __ may be removed this way.

 To avoid unfolding by mistake user's variables, we change
 the name of these generated let-in into "program_branch_NN" instead
 of "branch_NN"

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13964 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/subtac/subtac_cases.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/subtac')

diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 4f8344745e..cd4400f186 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -1738,7 +1738,7 @@ let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
 	 let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in
 	 let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
 	 and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
-	 let branch_name = id_of_string ("branch_" ^ (string_of_int !i)) in
+	 let branch_name = id_of_string ("program_branch_" ^ (string_of_int !i)) in
 	 let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in
 	 let branch =
 	   let bref = GVar (dummy_loc, branch_name) in
-- 
cgit v1.2.3