diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-28 17:45:48 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-28 17:45:48 +0000 |
| commit | d491c4974ad7ec82a5369049c27250dd07de852c (patch) | |
| tree | e00857f10948fcf48f5688b96a3a24fb7d67700c /plugins/funind/merge.ml | |
| parent | d5b03d4b052023012b859071e2bd6ff754256cab (diff) | |
Made that notations to names behave like the names they refer to wrt
implicit arguments and scope (use Implicit Arguments or Arguments
Scope commands instead if not the desired behaviour).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12439 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/funind/merge.ml')
0 files changed, 0 insertions, 0 deletions