diff options
| -rw-r--r-- | parsing/ppconstr.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index bb2a6ef54e..544a9fed5a 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -410,9 +410,9 @@ let gentermpr gt = (* [at_top] means ids of env must be avoided in bound variables *) -(* let gentermpr_core at_top env t = gentermpr (Termast.ast_of_constr at_top env t) -*) +(* let gentermpr_core at_top env t = pr_constr (Constrextern.extern_constr at_top env t) +*) |