From e0153316e98c294f316290ed34be7adef7896cb5 Mon Sep 17 00:00:00 2001 From: Allan Blanchard <allan.blanchard@cea.fr> Date: Thu, 5 Nov 2020 10:29:40 +0100 Subject: [PATCH] Apply suggestion to src/plugins/wp/doc/manual/wp_plugin.tex --- src/plugins/wp/doc/manual/wp_plugin.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex index e507f1215de..d5285609c67 100644 --- a/src/plugins/wp/doc/manual/wp_plugin.tex +++ b/src/plugins/wp/doc/manual/wp_plugin.tex @@ -306,7 +306,7 @@ $$\TACTIC{\Delta\models\,G}{% \end{array}} $$ \paragraph{Definition} Unfold predicate and logic function definition\\ -The user simply select a term $f(e_1,\ldots,e_n)$ or a predicate $P(e_1,\ldots,e_n)$ which is replaced by its definition, when available. +The user simply select a term $f(e_1,\ldots,e_n)$ or a predicate $P(e_1,\ldots,e_n)$ which is replaced with its definition, when available. \paragraph{Filter} Erase Hypotheses \\ The tactic is always applicable. It removes hypotheses from the goal on a variable used basis. When variables are compounds (record and arrays) a finer heuristics is used to detect which parts of the variable is relevant. A transitive closure of dependencies is also used. However, it is always possible that too many hypotheses are removed. -- GitLab