diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tactic_debug.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 4bf81f7ae2..5d2cbd57b8 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -142,9 +142,9 @@ let db_mc_pattern_success debug = str "Let us execute the right-hand side part..." ++ fnl()) let pp_match_pattern env = function - | Term c -> Term (extern_pattern env (names_of_rel_context env) c) + | Term c -> Term (extern_constr_pattern (names_of_rel_context env) c) | Subterm (o,c) -> - Subterm (o,(extern_pattern env (names_of_rel_context env) c)) + Subterm (o,(extern_constr_pattern (names_of_rel_context env) c)) (* Prints a failure message for an hypothesis pattern *) let db_hyp_pattern_failure debug env (na,hyp) = |