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.mli | |
| 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.mli')
| -rw-r--r-- | parsing/printer.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/printer.mli b/parsing/printer.mli index ca91cfd4f6..6a256bd599 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -76,6 +76,7 @@ val pr_global_env : Idset.t -> global_reference -> std_ppcmds val pr_global : global_reference -> std_ppcmds val pr_constant : env -> constant -> std_ppcmds +val pr_existential_key : existential_key -> std_ppcmds val pr_existential : env -> existential -> std_ppcmds val pr_constructor : env -> constructor -> std_ppcmds val pr_inductive : env -> inductive -> std_ppcmds |