diff options
author | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-29 19:23:25 +0000 |
---|---|---|
committer | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-29 19:23:25 +0000 |
commit | b20e1be71f9b5c5585b214e30b5042676fa6cd46 (patch) | |
tree | 6e9b6b6078d69420ee90751377d2f015fd8f1323 /parsing/pretty.ml | |
parent | 50457d3bf6aee2a49dd9c0acf7389b885178ea3f (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.ml | 3 |
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) |