Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • why3 why3
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Graph
    • Compare
  • Issues 165
    • Issues 165
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 25
    • Merge requests 25
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • Why3Why3
  • why3why3
  • Issues
  • #235
Closed
Open
Issue created Nov 13, 2018 by DAILLER Sylvain@sdaillerDeveloper

Avoid substituting to proxy symbols

When using subst_all or split_vc, it is not rare to substitute variables to a proxy symbol:

H : r = (o [@mlw_proxy_symbol])
Goal : r + r = 5

With subst_all or split_vc would become:

Goal: o + o = 5

I think it is better to do the substitution from the other side.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking