Auto merge of #704 - spastorino:small-fixes-on-engine, r=jackh726

Small fixes on engine

r? `@jackh726`

Author: bors

book/src/engine/logic.md

@@ -23,9 +23,9 @@ something to be unsolvable), the solving is restarted at the root `Goal`.
 In order to detect cycles (talked more about later), as well as keep track of
 the selected [`Strand`] for each table, `chalk-engine` stores a [`Stack`] on the
 `Forest`. Whenever a new goal is selected, a [`StackEntry`] is pushed onto the
-`Stack`, as well as the the "time" (which also gets incremented) that it was
-pushed. This "time" can be compared later to check if all the `Strands` of a
-[`Table`] have been checked in a single solve.
+`Stack`, as well as the "time" (which also gets incremented) that it was pushed.
+This "time" can be compared later to check if all the `Strands` of a [`Table`]
+have been checked in a single solve.
 
 As either `Answer`s are found for the selected `Table`, entries on the stack are
 `pop`ed. If something is found to be unsolvable, the complete stack is unwound.
@@ -34,7 +34,7 @@ As either `Answer`s are found for the selected `Table`, entries on the stack are
 
 As mentioned before, whenever a new `Goal` is encountered, a new [`Table`] is
 created to store current and future answers. First, the [`Goal`] is converted into
-an `HhGoal`. If it can be simplified, then a `Strand` with one or more
+an `GoalData`. If it can be simplified, then a `Strand` with one or more
 subgoals will be generated and can be followed as above. Otherwise, if it is a
 `DomainGoal` (see above), then
 [`program_clauses_for_goal`](https://rust-lang.github.io/chalk/chalk_solve/clauses/fn.program_clauses_for_goal.html)

book/src/engine/major_concepts.md

@@ -7,14 +7,14 @@ logic.
 ## Goals
 
 A "goal" in Chalk can be thought of as "something we want to prove". The engine
-itself understands `HhGoal`s. `HHGoal`s consist of the most basic logic,
+itself understands `GoalData`s. `GoalData`s consist of the most basic logic,
 such as introducing Binders (`Forall` or `Exists`) or combining goals (`All`).
 On the other hand, `Goal` represents an opaque goal generated
 externally. As such, it may contain any extra information or may be interned.
 When solving a logic predicate, Chalk will lazily convert `Goal`s
-into `HHGoal`s.
+into `GoalData`s.
 
-There are three types of completely opaque `HhGoal`s that Chalk can solve:
+There are three types of completely opaque `GoalData`s that Chalk can solve:
 `Unify`, `DomainGoal`, and `CannotProve`. Unlike the other types of goals,
 these three cannot be simplified any further. `Unify` is the goal of unifying
 any two types. `DomainGoal` is any goal that can solve by applying a