diff options
| author | Jim Fehrle | 2020-10-11 18:39:16 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-10-27 12:15:35 -0700 |
| commit | b402adc12c00ba72046423d3a1737ccad517f70e (patch) | |
| tree | 1940efc064bf87b9b996a0e21eaa75e9b57605d4 /vernac | |
| parent | 5f5cddae48c08872107f30938dcc2f3c8d91f33a (diff) | |
Rename operconstr -> term
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/egramcoq.ml | 4 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 4 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 6 |
3 files changed, 7 insertions, 7 deletions
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index b134f7b82b..123ea2c24e 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -300,13 +300,13 @@ let interp_constr_entry_key : type r. _ -> r target -> int -> r Entry.t * int op match forpat with | ForConstr -> if level = 200 then Constr.binder_constr, None - else Constr.operconstr, Some level + else Constr.term, Some level | ForPattern -> Constr.pattern, Some level let target_entry : type s. notation_entry -> s target -> s Entry.t = function | InConstrEntry -> (function - | ForConstr -> Constr.operconstr + | ForConstr -> Constr.term | ForPattern -> Constr.pattern) | InCustomEntry s -> let (entry_for_constr, entry_for_patttern) = find_custom_entry s in diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index dfc7b05b51..4c08cf7f79 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -687,7 +687,7 @@ GRAMMAR EXTEND Gram { VernacContext (List.flatten c) } | IDENT "Instance"; namesup = instance_name; ":"; - t = operconstr LEVEL "200"; + t = term LEVEL "200"; info = hint_info ; props = [ ":="; "{"; r = record_declaration; "}" -> { Some (true,r) } | ":="; c = lconstr -> { Some (false,c) } | -> { None } ] -> @@ -837,7 +837,7 @@ GRAMMAR EXTEND Gram (* Hack! Should be in grammar_ext, but camlp5 factorizes badly *) | IDENT "Declare"; IDENT "Instance"; id = ident_decl; bl = binders; ":"; - t = operconstr LEVEL "200"; + t = term LEVEL "200"; info = hint_info -> { VernacDeclareInstance (id, bl, t, info) } 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" -> |