diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/changes.txt | 13 | ||||
| -rw-r--r-- | dev/doc/proof-engine.md | 7 |
2 files changed, 16 insertions, 4 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index bcda4ff50a..0728608f31 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 db69b08a20..8f96ac223f 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 |