aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pretty.ml
diff options
context:
space:
mode:
authorGravatar delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-12-29 19:23:25 +0000
committerGravatar delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-12-29 19:23:25 +0000
commitb20e1be71f9b5c5585b214e30b5042676fa6cd46 (patch)
tree6e9b6b6078d69420ee90751377d2f015fd8f1323 /parsing/pretty.ml
parent50457d3bf6aee2a49dd9c0acf7389b885178ea3f (diff)
Ajout du Let pour le langage de tactiques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1231 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/pretty.ml')
-rw-r--r--parsing/pretty.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 33c5f862e..007a2e4ab 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -434,7 +434,8 @@ let inspect depth =
open Classops
-let string_of_strength = function
+let string_of_strength = function
+ | NotDeclare -> "(temp)"
| NeverDischarge -> "(global)"
| DischargeAt sp -> "(disch@"^(string_of_dirpath sp)