diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/changes.txt | 13 | ||||
| -rw-r--r-- | dev/doc/proof-engine.md | 7 | ||||
| -rw-r--r-- | dev/doc/setup.txt | 8 |
3 files changed, 19 insertions, 9 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index bcda4ff50..0728608f3 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -10,6 +10,16 @@ will fail to compile now. They should switch to `Bytes.t` * ML API * +Added two functions for declaring hooks to be executed in reduction +functions when some given constants are traversed: + + declare_reduction_effect: to declare a hook to be applied when some + constant are visited during the execution of some reduction functions + (primarily cbv). + + set_reduction_effect: to declare a constant on which a given effect + hook should be called. + We renamed the following functions: Context.Rel.Declaration.fold -> Context.Rel.Declaration.fold_constr @@ -144,6 +154,9 @@ In Coqlib / reference location: - The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase was very specific. Use tclPROGRESS instead. +- The unsafe flag of the Refine.refine function and its variants has been + renamed and dualized into typecheck and has been made mandatory. + ** Ltac API ** Many Ltac specific API has been moved in its own ltac/ folder. Amongst other diff --git a/dev/doc/proof-engine.md b/dev/doc/proof-engine.md index db69b08a2..8f96ac223 100644 --- a/dev/doc/proof-engine.md +++ b/dev/doc/proof-engine.md @@ -42,14 +42,13 @@ goal holes thanks to the `Refine` module, and in particular to the `Refine.refine` primitive. ```ocaml -val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic -(** In [refine ?unsafe t], [t] is a term with holes under some +val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic +(** In [refine typecheck t], [t] is a term with holes under some [evar_map] context. The term [t] is used as a partial solution for the current goal (refine is a goal-dependent tactic), the new holes created by [t] become the new subgoals. Exceptions raised during the interpretation of [t] are caught and result in - tactic failures. If [unsafe] is [false] (default is [true]) [t] is - type-checked beforehand. *) + tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *) ``` In a first approximation, we can think of `'a Sigma.run` as diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt index 1b016a4e2..0c6d3ee80 100644 --- a/dev/doc/setup.txt +++ b/dev/doc/setup.txt @@ -12,7 +12,7 @@ How to compile Coq Getting build dependencies: - sudo apt-get install make opam git mercurial darcs + sudo apt-get install make opam git opam init --comp 4.02.3 # Then follow the advice displayed at the end as how to update your ~/.bashrc and ~/.ocamlinit files. @@ -41,7 +41,7 @@ Building coqtop: cd ~/git/coq git checkout trunk make distclean - ./configure -annotate -with-doc no -local -debug -usecamlp5 + ./configure -annotate -local make clean make -j4 coqide printers @@ -49,8 +49,6 @@ The "-annotate" option is essential when one wants to use Merlin. The "-local" option is useful if one wants to run the coqtop and coqide binaries without running make install -The "-debug" option is essential if one wants to use ocamldebug with the coqtop binary. - Then check if - bin/coqtop - bin/coqide @@ -60,7 +58,7 @@ behave as expected. A note about rlwrap ------------------- -Running "coqtop" under "rlwrap" is possible, but there is a catch. If you try: +Running "coqtop" under "rlwrap" is possible, but (on Debian) there is a catch. If you try: cd ~/git/coq rlwrap bin/coqtop |