aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorgareuselesinge2011-11-21 17:03:54 +0000
committergareuselesinge2011-11-21 17:03:54 +0000
commit39fd2b160dbbd6411dd05f52984f198338de300a (patch)
treefba087dc2d603fc969c8b6193662f01ffcc9f08f /dev
parented06a90f16fcf7d45672bbddf42efe4cc0efd4d4 (diff)
Renamig support added to "Arguments"
Example: Arguments eq_refl {B y}, [B] y. Check (eq_refl (B := nat)). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14719 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
-rw-r--r--dev/printers.mllib1
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 4df8b9cc48..6a42678e4f 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -80,6 +80,7 @@ Evarutil
Term_dnet
Recordops
Evarconv
+Arguments_renaming
Typing
Pattern
Matching