diff options
| author | Pierre-Marie Pédrot | 2018-09-30 18:03:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-30 18:03:48 +0200 |
| commit | c155259dee7e4b2bfafe42375b45f2f4d6c6cfbd (patch) | |
| tree | 61155d86c6460059c5ebaa87e74202589fde5d3d /dev | |
| parent | a87f76337e2473e2de15cffb058ea3087e6a532f (diff) | |
| parent | fa515984a105b523a92394578a8afc55d0e95c5d (diff) | |
Merge PR #8599: Typo in top_printers.ml
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/top_printers.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index ced6ea2614..e15fd776b2 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -139,7 +139,7 @@ let safe_pr_global = function | ConstRef kn -> pp (str "CONSTREF(" ++ Constant.debug_print kn ++ str ")") | IndRef (kn,i) -> pp (str "INDREF(" ++ MutInd.debug_print kn ++ str "," ++ int i ++ str ")") - | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ MutInd.debug_print kn ++ str "," ++ + | ConstructRef ((kn,i),j) -> pp (str "CONSTRUCTREF(" ++ MutInd.debug_print kn ++ str "," ++ int i ++ str "," ++ int j ++ str ")") | VarRef id -> pp (str "VARREF(" ++ Id.print id ++ str ")") |