diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/changes.txt | 2 | ||||
| -rw-r--r-- | dev/include | 2 |
2 files changed, 3 insertions, 1 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index feef80ed35..fcee79e07e 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -248,6 +248,8 @@ define_evar_* mostly used internally in the unification engine. open Proofview.Notations Proofview.Goal.enter { enter = begin fun gl -> ... end } + +- `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)` --> `Tacinterp.Value.of_constr c` ========================================= = CHANGES BETWEEN COQ V8.4 AND COQ V8.5 = diff --git a/dev/include b/dev/include index b2eb280d6c..d82fb74f22 100644 --- a/dev/include +++ b/dev/include @@ -25,7 +25,7 @@ #cd ".";; #use "base_include";; -#install_printer (* pp_stdcmds *) pppp;; +#install_printer (* pp_stdcmds *) pp;; #install_printer (* pattern *) pppattern;; #install_printer (* glob_constr *) ppglob_constr;; |