From 166a8c2e15dfa43c3178f70d515dfde1c5f15fad Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 4 Jul 2016 14:58:59 -0700 Subject: Add a renaming of Tacexpr.TacDynamic --- dev/doc/changes.txt | 2 ++ 1 file changed, 2 insertions(+) (limited to 'dev') diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 3cd371bfdc..b0f9ae2c38 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 = -- cgit v1.2.3 From 6afe9005b2f050e04f897ed7e84014058fc94e4b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 31 Jul 2016 07:51:08 +0200 Subject: A fix to dev/include. --- dev/include | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dev') 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;; -- cgit v1.2.3