RODIN / Bugs / #415 RBP allows to generate theory with same name as a context

#415 RBP allows to generate theory with same name as a context

Milestone: 1.2

Status: closed

Owner: Issam

Labels: Rule-based prover plugin (6)

Priority: 5

Updated: 2010-09-27

Created: 2010-03-05

Creator: wohuai

Private: No

The rule based prover (0.2.0) allows me to create a theory with the name of an existing context (maybe also machine).
The proof obligations of the context are then exactly the proof obligations of the theory.
It seems that the .bpr file of the theory overwrites / hides the .bpr file of the context.

Discussion

Carine Pascal - 2010-03-16

The issue is related to the rule-based prover plug-in.

If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Carine Pascal - 2010-03-16

labels: --> Rule-based prover plugin

assigned_to: nobody --> maamria
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Issam - 2010-03-23

This does not happen on Windows platform. What system are you using?

If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

wohuai - 2010-03-23

I use Linux.

If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Issam - 2010-09-27

The rule-based prover will be part of the theory plug-in that also defines the mathematical extensions. This problem should not appear in the release of Theory plug-in.

If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Issam - 2010-09-27

status: open --> closed
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

RBP allows to generate theory with same name as a context

Group

Searches

Help

#415 RBP allows to generate theory with same name as a context

Discussion