diff options
| author | letouzey | 2011-04-07 11:04:46 +0000 |
|---|---|---|
| committer | letouzey | 2011-04-07 11:04:46 +0000 |
| commit | 92a5f74259977cc3f92d8b822bdb727a95e64bc6 (patch) | |
| tree | fbe2bd20200ac9de7c89c6a8752f3f007ed06b30 /plugins/subtac | |
| parent | 5de2bbd213eb770ba465c67103004d9286444a63 (diff) | |
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
Diffstat (limited to 'plugins/subtac')
| -rw-r--r-- | plugins/subtac/subtac_cases.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |