aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/tacinterp.mli2
1 files changed, 1 insertions, 1 deletions
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