From 1053c873bdaedf37c1fd35be4e7021bfc806c23d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 16 Nov 2016 11:17:39 +0100 Subject: [doc] Mention XML protocol on changes. It may be worth it, also added a note about file reorganization. --- dev/doc/changes.txt | 2 ++ 1 file changed, 2 insertions(+) (limited to 'dev/doc') diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 79a0c6312a..d052468f99 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -14,6 +14,8 @@ kernel/closure.ml{,i} -> kernel/cClosure.ml{,i} lib/errors.ml{,i} -> lib/cErrors.ml{,i} toplevel/cerror.ml{,i} -> toplevel/explainErr.mli{,i} +All IDE-specific files, including the XML protocol have been moved to ide/ + ** Reduction functions ** In closure.ml, we introduced the more precise reduction flags fMATCH, fFIX, -- cgit v1.2.3 From 27190db7f119bc9b50150be6dff889986c747e38 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 21 Nov 2016 15:05:26 -0500 Subject: (v8.6) Add example in dev/doc/changes involving Tacmach.project --- dev/doc/changes.txt | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'dev/doc') diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index d052468f99..e926674696 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -244,6 +244,10 @@ define_evar_* mostly used internally in the unification engine. ... let Sigma (xn, sigma, pn) = ... in Sigma (ans, sigma, p1 +> ... +> pn) + + Examples of `Sigma.Unsafe.of_evar_map` include: + + Evarutil.new_evar env (Tacmach.project goal) ty ----> Evarutil.new_evar env (Sigma.Unsafe.of_evar_map (Tacmach.project goal)) ty - The Proofview.Goal.*enter family of functions now takes a polymorphic continuation given as a record as an argument. -- cgit v1.2.3 From 8572140c30629cfcc6b7e68d450487c64922a6b9 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 21 Nov 2016 16:01:34 -0500 Subject: (v8.6) Make a note about wit_constr and Constrarg in dev/doc/changes --- dev/doc/changes.txt | 2 ++ 1 file changed, 2 insertions(+) (limited to 'dev/doc') diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index d052468f99..12c0163b95 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -218,6 +218,8 @@ val get_id_for_feedback : unit -> edit_or_state_id * route_id for constructing compound entries still works over this scheme. Note that in the case of (VERNAC) ARGUMENT EXTEND, the name of the argument entry is bound in the parsing rules, so beware of recursive calls. + + For example, to get "wit_constr" you must "open Constrarg" at the top of the file. - Evarutil was split in two parts. The new Evardefine file exposes functions define_evar_* mostly used internally in the unification engine. -- cgit v1.2.3 From 59dee24e5dfe3dfe20c2a4a2843192d797c89155 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 21 Nov 2016 17:03:22 -0500 Subject: (v8.6) Update dev/doc/changes with things about mem_named_context --- dev/doc/changes.txt | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'dev/doc') diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index d052468f99..156f38c455 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -256,7 +256,10 @@ define_evar_* mostly used internally in the unification engine. Proofview.Goal.enter { enter = begin fun gl -> ... end } -- `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)` --> `Tacinterp.Value.of_constr c` +- `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)` ---> `Tacinterp.Value.of_constr c` +- `Pretyping.Termops.mem_named_context` ---> `Engine.Termops.mem_named_context_val` + (`Global.named_context` ---> `Global.named_context_val`) + (`Context.Named.lookup` ---> `Environ.lookup_named_val`) ** Search API ** -- cgit v1.2.3 From bfa2ac5fc5578d9bcf2ea1183deeaa6329c29b9b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 21 Nov 2016 17:11:45 -0500 Subject: (v8.6) Update dev/doc/changes.txt with HintsResolveEntry changes --- dev/doc/changes.txt | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'dev/doc') diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index d052468f99..134a6a25e8 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -256,7 +256,8 @@ define_evar_* mostly used internally in the unification engine. Proofview.Goal.enter { enter = begin fun gl -> ... end } -- `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)` --> `Tacinterp.Value.of_constr c` +- `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)` ---> `Tacinterp.Value.of_constr c` +- `Vernacexpr.HintsResolveEntry(priority, poly, hnf, path, atom)` ---> `Vernacexpr.HintsResolveEntry(Vernacexpr.({hint_priority = priority; hint_pattern = None}), poly, hnf, path, atom)` ** Search API ** -- cgit v1.2.3 From a27ac0315dcbb99c64a260bac3988199a26b39cf Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 24 Nov 2016 15:14:19 +0100 Subject: Fix some documentation typos. Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else. --- dev/doc/notes-on-conversion | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dev/doc') diff --git a/dev/doc/notes-on-conversion b/dev/doc/notes-on-conversion index 6274275c9d..a81f170c63 100644 --- a/dev/doc/notes-on-conversion +++ b/dev/doc/notes-on-conversion @@ -21,7 +21,7 @@ Notation OMEGA := (ack 4 4). Definition f (x:nat) := x. -(* Evaluation in tactics can somehow be controled *) +(* Evaluation in tactics can somehow be controlled *) Lemma l1 : OMEGA = OMEGA. reflexivity. (* succeed: identity *) Qed. (* succeed: identity *) -- cgit v1.2.3