From b31b48407a9f5d36cefd6dec3ddf3e0b8391f14c Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 29 May 2012 11:08:41 +0000
Subject: Tacexpr as a mli-only, the few functions there are now in Tacops

 NB: former Tacexpr.no_move is now Tacexpr.MoveLast
  (when introducing, intro with no move is intro as last)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15373 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/printers.mllib | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 8ba2070000..436fa287f4 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -115,7 +115,7 @@ Smartlocate
 Constrintern
 Modintern
 Constrextern
-Tacexpr
+Tacops
 Proof_type
 Goal
 Logic
-- 
cgit v1.2.3