From d1f4bd9451517a4dd2cca438adbeea69c1d6fb62 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 27 Jan 2001 17:13:42 +0000
Subject: make doc

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

(limited to 'proofs')

diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index 83cd7be1c2..7d066e8987 100644
--- a/proofs/tacinterp.mli
+++ b/proofs/tacinterp.mli
@@ -22,7 +22,7 @@ type value =
   | VVoid
   | VRec of value ref
 
-(* Signature for interpretation: val_interp and interpretation functions *)
+(* Signature for interpretation: val\_interp and interpretation functions *)
 and interp_sign =
   enamed_declarations * Environ.env * (string * value) list *
     (int * constr) list * goal sigma option * debug_info
-- 
cgit v1.2.3