Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
a8564b0d
Commit
a8564b0d
authored
Feb 14, 2018
by
Sylvain Dailler
Browse files
copy/paste of proof tree: allow pasting on an ancestor. fix#89
parent
d0a73309
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/session/controller_itp.ml
View file @
a8564b0d
...
...
@@ -872,8 +872,8 @@ let rec copy_rec ~notification ~callback_pa ~callback_tr c from_any to_any =
let
copy_paste
~
notification
~
callback_pa
~
callback_tr
c
from_any
to_any
=
let
s
=
c
.
controller_session
in
if
is_below
s
from_any
to_any
||
is_below
s
to_any
from_any
then
raise
BadCopyPaste
;
if
is_below
s
to_any
from_any
then
raise
BadCopyPaste
;
match
from_any
,
to_any
with
|
APn
_
,
APn
_
->
copy_rec
~
notification
~
callback_pa
~
callback_tr
c
from_any
to_any
...
...
DAILLER Sylvain
@sdailler
mentioned in issue
#89 (closed)
·
Feb 14, 2018
mentioned in issue
#89 (closed)
mentioned in issue #89
Toggle commit list
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment