diff options
Diffstat (limited to 'parsing/printer.ml')
| -rw-r--r-- | parsing/printer.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index f777a37edf..dd8264ea77 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -458,6 +458,13 @@ let pr_prim_rule = function | Rename (id1,id2) -> (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2) + | Change_evars -> + (* This is internal tactic and cannot be replayed at user-level. + Function pr_rule_dot below is used when we want to hide + Change_evars *) + str "Evar change" + + (* Backwards compatibility *) let prterm = pr_lconstr |