diff options
| author | herbelin | 2005-01-02 08:47:14 +0000 |
|---|---|---|
| committer | herbelin | 2005-01-02 08:47:14 +0000 |
| commit | 2dee039338e6f130447741b67f36eba666131b8a (patch) | |
| tree | b7ac63eb7f7cc87edfa0056e7c69653fd6c802a1 /translate | |
| parent | da705691fc9cf7724f78f4ed0cc8b93c4d7bc08e (diff) | |
Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de printers dans ocamldebug
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6546 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppconstrnew.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index 846b6468c3..6bae2537ed 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -71,7 +71,7 @@ let decode_patlist_value = function | CPatCstr (_,_,l) -> l | _ -> anomaly "Ill-formed list argument of notation" -open Symbols +open Notation let rec print_hunk n decode pr env = function | UnpMetaVar (e,prec) -> pr (n,prec) (env_assoc_value e env) |