Skip to content

  • Projects
  • Groups
  • Snippets
  • Help
  • This project
    • Loading...
  • Sign in / Register
why3
why3
  • Overview
    • Overview
    • Details
    • Activity
    • Cycle Analytics
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Charts
  • Registry
  • Issues 31
    • Issues 31
    • List
    • Board
    • Labels
    • Milestones
  • Merge Requests 2
    • Merge Requests 2
  • CI / CD
    • CI / CD
    • Pipelines
    • Schedules
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Charts
  • Create a new issue
  • Commits
  • Issue Boards
  • Why3
  • why3why3
  • Issues
  • #52

Closed
Open
Opened Dec 14, 2017 by CLOCHARD Martin@mclochar 
  • Report abuse
  • New issue
Report abuse New issue

warning when cloning module containing only "val"s as abstract symbols

When cloning a module where all abstract symbols are val, like

module A0
  val f () : unit
end
module A1
  let f () = ()
  clone A0 with val f = f
end

Why3 sends the warning cloned theory .A0 does not contain any abstract symbol; it should be used instead. However, A0 does contain an abstract symbol.

Edited Mar 06, 2018 by Guillaume Melquiond
Assignee
Assign to
New system
Milestone
New system
Assign milestone
Time tracking
None
Due date
No due date
0
Labels
None
Assign labels
  • View labels
Reference: why3/why3#52