aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-12-14 01:47:44 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-12-14 01:47:44 +0000
commitde4389d0f4849a9ad897f2fc3aecd7e2fa58ffcc (patch)
tree7101e54c72cf985bf660d0f022414db34a25940b
parent7af0ff6260649d51e75b5427ada01ca0d8fd897b (diff)
Enfin trouvé la cause d'exception; suppression de la capsule de rattrapage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1102 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--dev/top_printers.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 4f0717b85..0a6b58489 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -15,6 +15,7 @@ open Tacmach
open Term
open Vernacinterp
open Clenv
+open Errors
let _ = Termast.print_evar_arguments := true
@@ -24,7 +25,7 @@ let prast c = pP(print_ast c)
let prastpat c = pP(print_astpat c)
let prastpatl c = pP(print_astlpat c)
-let ppterm = (fun x -> pP(prterm x))
+let ppterm = (fun x -> pP(prterm x)
let pprawterm = (fun x -> pP(pr_rawterm x))
let pppattern = (fun x -> pP(pr_pattern x))
let pptype = (fun x -> pP(prtype x))