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 57e813632..fb99e8dd6 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -410,10 +410,10 @@ 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) -*) |