From b402adc12c00ba72046423d3a1737ccad517f70e Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sun, 11 Oct 2020 18:39:16 -0700
Subject: Rename operconstr -> term

---
 vernac/metasyntax.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'vernac/metasyntax.ml')

diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 8ce59c40c3..185abcf35b 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -61,15 +61,15 @@ let pr_registered_grammar name =
     prlist pr_one entries
 
 let pr_grammar = function
-  | "constr" | "operconstr" | "binder_constr" ->
+  | "constr" | "term" | "binder_constr" ->
       str "Entry constr is" ++ fnl () ++
       pr_entry Pcoq.Constr.constr ++
       str "and lconstr is" ++ fnl () ++
       pr_entry Pcoq.Constr.lconstr ++
       str "where binder_constr is" ++ fnl () ++
       pr_entry Pcoq.Constr.binder_constr ++
-      str "and operconstr is" ++ fnl () ++
-      pr_entry Pcoq.Constr.operconstr
+      str "and term is" ++ fnl () ++
+      pr_entry Pcoq.Constr.term
   | "pattern" ->
       pr_entry Pcoq.Constr.pattern
   | "vernac" ->
-- 
cgit v1.2.3