diff options
Diffstat (limited to 'parsing/pptactic.ml')
| -rw-r--r-- | parsing/pptactic.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index c7e1db60..c68a2d6f 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pptactic.ml 9319 2006-10-30 12:41:21Z barras $ *) +(* $Id: pptactic.ml 9551 2007-01-29 15:13:35Z bgregoir $ *) open Pp open Names @@ -652,6 +652,7 @@ and pr_atom1 = function | TacAssumption as t -> pr_atom0 t | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c) | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c) + | TacVmCastNoCheck c -> hov 1 (str "vm_cast_no_check" ++ pr_constrarg c) | TacApply cb -> hov 1 (str "apply" ++ spc () ++ pr_with_bindings cb) | TacElim (cb,cbo) -> hov 1 (str "elim" ++ pr_arg pr_with_bindings cb ++ |