From 4638e487738118ef79d90f1f0b262d6beb98d974 Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 12 Nov 2003 03:06:27 +0000 Subject: deux doigts d'extraction dans le CHANGES pour la V8 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4859 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CHANGES | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/CHANGES b/CHANGES index 00e576ec4e..9c19bc83e2 100644 --- a/CHANGES +++ b/CHANGES @@ -142,6 +142,14 @@ Tactics longer an immediate hint), resulting in shorter proofs and subgoals proved more easily +Extraction (See details in contrib/extraction/CHANGES) + +- The old commands: (Recursive) Extraction Module M. + are now: (Recursive) Extraction Library M. + To use these commands, M should come from a library M.v +- The other syntax Extraction & Recursive Extraction now accept + module names as arguments. + Bugs - Rename bug fixed (#244) -- cgit v1.2.3