diff options
| author | herbelin | 2011-03-07 20:11:32 +0000 |
|---|---|---|
| committer | herbelin | 2011-03-07 20:11:32 +0000 |
| commit | 6cbd65aa4e5fe82259b44b89e5e624ed2299249c (patch) | |
| tree | ee4b6d9b9430519bfc153a405e88edc9b2ced2e7 /parsing/printer.ml | |
| parent | 0176dd0d2d657867c7ecc93fc979dc15c1409336 (diff) | |
Added propagation of evars unification failure reasons for better
error messages. The architecture of unification error handling
changed, not helped by ocaml for checking that every exceptions is
correctly caught. Report or fix if you find a regression.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13893 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/printer.ml')
| -rw-r--r-- | parsing/printer.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index f1f5d4c9f3..27dcffceae 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -120,6 +120,7 @@ let pr_global_env = pr_global_env let pr_global = pr_global_env Idset.empty let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst) +let pr_existential_key evk = str (string_of_existential evk) let pr_existential env ev = pr_lconstr_env env (mkEvar ev) let pr_inductive env ind = pr_lconstr_env env (mkInd ind) let pr_constructor env cstr = pr_lconstr_env env (mkConstruct cstr) |