guidelines: add a section about backward vs forward reasoning

17 jobs for pg in 13 minutes and 38 seconds (queued for 4 seconds)
Status Job ID Name Coverage
  Build
passed #80285
1.10.0-coq-8.10

00:12:18

passed #80286
1.10.0-coq-8.11

00:05:25

passed #80284
1.10.0-coq-8.9

00:05:16

passed #80282
1.9.0-coq-8.10

00:05:18

passed #80283
1.9.0-coq-8.11

00:12:18

passed #80281
1.9.0-coq-8.9

00:12:18

passed #80287
build-for-process

00:04:31

passed #80288
build-for-process-classic

00:07:54

failed #80291
allowed to fail
coq-8.10

00:03:22

failed #80292
allowed to fail
coq-dev

00:06:10

passed #80289
proof-length

00:00:07

passed #80290
spell-check

00:00:14

 
  Process
passed #80295
doc

00:00:17

passed #80296
doc-classic

00:00:32

passed #80297
proof-state

00:03:46

passed #80293
validate

00:00:49

passed #80294
validate-classic

00:01:10

 
Name Stage Failure
failed
coq-dev Build


<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-prosa dev
+-
- No changes have been performed
'opam install -y -v -j 2 coq-prosa' failed.
ERROR: Job failed: exit code 1
failed
coq-8.10 Build
# File "./classic/model/schedule/uni/susp/build_suspension_table.v", line 229, characters 20-85:
# Error: Unknown interpretation for notation "@ arg_maxP".
#
# make[1]: *** [Makefile:676: classic/model/schedule/uni/susp/build_suspension_table.vo] Error 1
# make[1]: *** Waiting for unfinished jobs....
# make: *** [Makefile:321: all] Error 2

'opam install -y -v -j 2 coq-prosa' failed.
ERROR: Job failed: exit code 1