Imported Upstream version 8.0pl3+8.1beta.2upstream/8.0pl3+8.1beta.2

1 files changed, 21 insertions, 0 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index f60e3203..90e29496 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -13,11 +13,23 @@ Lib: library_part -> remove_section_part
 Printer: prterm -> pr_lconstr
 Printer: prterm_env -> pr_lconstr_env
 Ppconstr: pr_sort -> pr_rawsort
+Evd: in_dom, etc got standard ocaml names (i.e. mem, etc)
+Pretyping: 
+ - understand_gen_tcc and understand_gen_ltac merged into understand_ltac
+ - type_constraints can now say typed by a sort (use OfType to get the
+   previous behavior)
+Library: import_library -> import_module
 
 ** Constructors
 
 Declarations: mind_consnrealargs -> mind_consnrealdecls
 NoRedun -> NoDup
+Cast and RCast have an extra argument: you can recover the previous
+  behavior by setting the extra argument to "CastConv DEFAULTcast" and
+  "DEFAULTcast" respectively
+Names: "kernel_name" is now "constant" when argument of Term.Const
+Tacexpr: TacTrueCut and TacForward(false,_,_) merged into new TacAssert
+Tacexpr: TacForward(true,_,_) branched to TacLetTac
 
 ** Modules
 
@@ -27,11 +39,20 @@ module Tacred spawned module Redexpr
 module Symbols -> Notation
 module Coqast, Ast, Esyntax, Termast, and all other modules related to old
   syntax are removed
+module Instantiate: integrated to Evd
+module Pretyping now a functor: use Pretyping.Default instead
 
 ** Internal names
 
 OBJDEF and OBJDEF1 -> CANONICAL-STRUCTURE
 
+** Tactic extensions
+
+- printers have an extra parameter which is a constr printer at high precedence
+- the tactic printers have an extra arg which is the expected precedence 
+- level is now a precedence in declare_extra_tactic_pprule
+- "interp" functions now of types the actual arg type, not its encapsulation
+  as a generic_argument
 
 =========================================
 = CHANGES BETWEEN COQ V7.4 AND COQ V8.0 =