diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 2 | ||||
| -rw-r--r-- | dev/db | 2 | ||||
| -rw-r--r-- | dev/include | 2 | ||||
| -rw-r--r-- | dev/ocamldoc/docintro | 2 | ||||
| -rw-r--r-- | dev/top_printers.ml | 2 |
5 files changed, 5 insertions, 5 deletions
diff --git a/dev/base_include b/dev/base_include index 23cc38fb47..19c0f4b4e1 100644 --- a/dev/base_include +++ b/dev/base_include @@ -171,7 +171,7 @@ let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;; let parse_tac = Pcoq.parse_string Pcoq.Tactic.tactic;; let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;; -(* build a term of type rawconstr without type-checking or resolution of +(* build a term of type glob_constr without type-checking or resolution of implicit syntax *) let e s = @@ -17,7 +17,7 @@ install_printer Top_printers.ppclindex install_printer Top_printers.ppbigint install_printer Top_printers.pppattern -install_printer Top_printers.pprawconstr +install_printer Top_printers.ppglob_constr install_printer Top_printers.ppconstr install_printer Top_printers.ppuni diff --git a/dev/include b/dev/include index 251a969b9c..b72e68ac07 100644 --- a/dev/include +++ b/dev/include @@ -14,7 +14,7 @@ #install_printer (* pp_stdcmds *) pppp;; #install_printer (* pattern *) pppattern;; -#install_printer (* rawconstr *) pprawconstr;; +#install_printer (* glob_constr *) ppglob_constr;; #install_printer (* constr *) ppconstr;; #install_printer (* constr_substituted *) ppsconstr;; diff --git a/dev/ocamldoc/docintro b/dev/ocamldoc/docintro index 20c3de5efc..33d20fc818 100644 --- a/dev/ocamldoc/docintro +++ b/dev/ocamldoc/docintro @@ -30,7 +30,7 @@ describes the Coq library, which is made of two parts: describes the translation from Coq context-dependent front abstract syntax of terms {v constr_expr v} to and from the -context-free, untyped, globalized form of constructions {v rawconstr v}.} +context-free, untyped, globalized form of constructions {v glob_constr v}.} {- Parsers and printers : parsing describes the implementation of the Coq parsers and printers.} diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 1f05e90bde..89a6eb5e32 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -56,7 +56,7 @@ let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr x) let ppterm = ppconstr let ppsconstr x = ppconstr (Declarations.force x) let ppconstr_univ x = Constrextern.with_universes ppconstr x -let pprawconstr = (fun x -> pp(pr_lrawconstr x)) +let ppglob_constr = (fun x -> pp(pr_lglob_constr x)) let pppattern = (fun x -> pp(pr_constr_pattern x)) let pptype = (fun x -> try pp(pr_ltype x) with e -> pp (str (Printexc.to_string e))) |