diff options
| author | Matthieu Sozeau | 2014-08-18 16:44:10 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-08-18 17:10:00 +0200 |
| commit | 8d5238f09a6d7e0b8cb64a21d5d1410c519ff1ab (patch) | |
| tree | 6d689ecdb3a61b93f234c57e33b812b3d743742c /printing/pptactic.ml | |
| parent | c61e5783458d4b9f2cd104bd027893f6bdc82ded (diff) | |
Refine patch for behavior of unify_to_subterm to allow backtracking on
unsatisfiable constraint failures but give sensible error messages if
an occurrence was found and only typeclass resolution failed.
Fixes MathClasses.
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index e6157793e3..785b0e8dce 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -581,7 +581,7 @@ let make_pr_tac pr_tac_level pr_cst,pr_ind,pr_ref,pr_ident,pr_extend,pr_alias,strip_prod_binders, pr_gen) = (* some shortcuts *) -let pr_bindings = pr_bindings pr_constr pr_lconstr in +let _pr_bindings = pr_bindings pr_constr pr_lconstr in let pr_ex_bindings = pr_bindings_gen true pr_constr pr_lconstr in let pr_with_bindings = pr_with_bindings pr_constr pr_lconstr in let pr_with_bindings_arg = pr_with_bindings_arg pr_constr pr_lconstr in |