OCamllabs icon Home|Differences with the last checks|Previous runs


Building on asteria.caelum.ci.dev

(from ocaml/opam:debian-unstable)
Unable to find image 'ocaml/opam:debian-unstable' locally
debian-unstable: Pulling from ocaml/opam
Digest: sha256:bb63d24d162b67d0a5287c42134a96125ce1fd1724f856cf968e09dab5db3923
Status: Downloaded newer image for ocaml/opam:debian-unstable
2024-02-15 06:49.18 ---> using "0acd5aeaa8f7bc314514d9795d14a7f12ec72a6a5b11c5904350189734c6859b" from cache

/: (user (uid 1000) (gid 1000))

/: (env OPAMPRECISETRACKING 1)

/: (env OPAMUTF8 never)

/: (env OPAMEXTERNALSOLVER builtin-0install)

/: (env OPAMCRITERIA +removed)

/: (run (shell "sudo ln -f /usr/bin/opam-dev /usr/bin/opam"))
2024-02-15 06:49.18 ---> using "65c3237f501f7c75f3828458ecf2342bc41c98aaef8c6a7fd82bf46a58cb258c" from cache

/: (run (network host)
        (shell "rm -rf ~/opam-repository && git clone -q 'https://github.com/ocaml/opam-repository' ~/opam-repository && git -C ~/opam-repository checkout -q a2d9de3b60db9ca6abc14fbf7d4ed1206e1c206c"))
2024-02-15 06:49.18 ---> using "81ca8611ef22904e385d01ce08beaaae4b75616ac602e5536c5aa1b6a3d1d20f" from cache

/: (run (shell "rm -rf ~/.opam && opam init -ya --bare --config ~/.opamrc-sandbox ~/opam-repository"))
Configuring from /home/opam/.opamrc-sandbox, then /home/opam/.opamrc, and finally from built-in defaults.
Checking for available remotes: rsync and local, git.
  - you won't be able to use mercurial repositories unless you install the hg command on your system.
  - you won't be able to use darcs repositories unless you install the darcs command on your system.


<><> Fetching repository information ><><><><><><><><><><><><><><><><><><><><><>
[default] Initialised

User configuration:
  ~/.profile is already up-to-date.
[NOTE] Make sure that ~/.profile is well sourced in your ~/.bashrc.

2024-02-15 06:49.18 ---> using "53c7af86da149782029aa41361179b0566f5713cd76a5342c4b152b1f918729c" from cache

/: (run (cache (opam-archives (target /home/opam/.opam/download-cache)))
        (network host)
        (shell "opam switch create --repositories=default '4.10' '4.10.2'"))

<><> Installing new switch packages <><><><><><><><><><><><><><><><><><><><><><>
Switch invariant: ["ocaml-base-compiler" {= "4.10.2"} | "ocaml-system" {= "4.10.2"}]

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> installed base-bigarray.base
-> installed base-threads.base
-> installed base-unix.base
-> retrieved ocaml-base-compiler.4.10.2  (cached)
-> installed ocaml-base-compiler.4.10.2
-> installed ocaml-config.1
-> installed ocaml.4.10.2
Done.
# Run eval $(opam env --switch=4.10) to update the current shell environment
2024-02-15 06:49.18 ---> using "fad1eddbe29ab6e53b9b09b59f9821d2132d9b2121edda3e26e7e9917bbdd9cb" from cache

/: (run (network host)
        (shell "opam update --depexts"))
+ /usr/bin/sudo "apt-get" "update"
- Get:1 http://deb.debian.org/debian unstable InRelease [198 kB]
- Get:2 http://deb.debian.org/debian unstable/main amd64 Packages.diff/Index [63.6 kB]
- Get:3 http://deb.debian.org/debian unstable/main amd64 Packages T-2024-02-14-1406.13-F-2024-02-09-1406.14.pdiff [513 kB]
- Get:3 http://deb.debian.org/debian unstable/main amd64 Packages T-2024-02-14-1406.13-F-2024-02-09-1406.14.pdiff [513 kB]
- Fetched 774 kB in 1s (546 kB/s)
- Reading package lists...
- 
2024-02-15 06:49.18 ---> using "d87035ee056a8096163f4a820f831899624da8c0a841cded8336607399f533ed" from cache

/: (run (cache (opam-archives (target /home/opam/.opam/download-cache)))
        (network host)
        (shell  "\
               \nopam remove -y \"ott.0.27\"\
               \nopam install -vy \"ott.0.27\"\
               \nres=$?\
               \nif [ $res = 31 ]; then\
               \n    if opam show -f x-ci-accept-failures: \"ott.0.27\" | grep -q '\"debian-unstable\"'; then\
               \n        echo \"This package failed and has been disabled for CI using the 'x-ci-accept-failures' field.\"\
               \n        exit 69\
               \n    fi\
               \nfi\
               \n\
               \n\
               \nexit $res\
               \n"))
[NOTE] ott.0.27 is not installed.

Nothing to do.
The following actions will be performed:
=== install 1 package
  - install ott 0.27

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  1/3:
-> retrieved ott.0.27  (cached)
Processing  2/3: [ott: make world]
+ /home/opam/.opam/opam-init/hooks/sandbox.sh "build" "make" "world" (CWD=/home/opam/.opam/4.10/.opam-switch/build/ott.0.27)
- cd src; make install
- make[1]: Entering directory '/home/opam/.opam/4.10/.opam-switch/build/ott.0.27/src'
- ocamllex grammar_lexer.mll
- 374 states, 16439 transitions, table size 68000 bytes
- 3397 additional bytes used for bindings
- ocamlyacc -v grammar_parser.mly
- 2 rules never reduced
- ocamldep location.ml types.ml auxl.ml merge.ml global_option.ml grammar_lexer.ml grammar_parser.mli grammar_parser.ml version.ml grammar_pp.ml parse_table.ml glr.ml new_term_parser.ml term_parser.ml dependency.ml bounds.ml context_pp.ml quotient_rules.ml grammar_typecheck.ml transform.ml substs_pp.ml subrules_pp.ml embed_pp.ml defns.ml ln_transform.ml coq_induct.ml system_pp.ml lex_menhir_pp.ml align.ml main.ml align.mli bounds.mli coq_induct.mli defns.mli dependency.mli embed_pp.mli grammar_typecheck.mli merge.mli subrules_pp.mli substs_pp.mli system_pp.mli lex_menhir_pp.mli transform.mli term_parser.mli > .depend
- mkdir ../bin
- cd .. && tar -zxvf ocamlgraph-1.7.tar.gz
- ocamlgraph-1.7/
- ocamlgraph-1.7/bin/
- ocamlgraph-1.7/src/
- ocamlgraph-1.7/src/blocks.ml
- ocamlgraph-1.7/src/builder.ml
- ocamlgraph-1.7/src/builder.mli
- ocamlgraph-1.7/src/classic.ml
- ocamlgraph-1.7/src/classic.mli
- ocamlgraph-1.7/src/cliquetree.ml
- ocamlgraph-1.7/src/cliquetree.mli
- ocamlgraph-1.7/src/coloring.ml
- ocamlgraph-1.7/src/coloring.mli
- ocamlgraph-1.7/src/components.ml
- ocamlgraph-1.7/src/components.mli
- ocamlgraph-1.7/src/delaunay.ml
- ocamlgraph-1.7/src/delaunay.mli
- ocamlgraph-1.7/src/dot.ml
- ocamlgraph-1.7/src/dot.mli
- ocamlgraph-1.7/src/dot_ast.mli
- ocamlgraph-1.7/src/dot_lexer.ml
- ocamlgraph-1.7/src/dot_lexer.mll
- ocamlgraph-1.7/src/dot_parser.ml
- ocamlgraph-1.7/src/dot_parser.mli
- ocamlgraph-1.7/src/dot_parser.mly
- ocamlgraph-1.7/src/flow.ml
- ocamlgraph-1.7/src/flow.mli
- ocamlgraph-1.7/src/gmap.ml
- ocamlgraph-1.7/src/gmap.mli
- ocamlgraph-1.7/src/gml.ml
- ocamlgraph-1.7/src/gml.mli
- ocamlgraph-1.7/src/gml.mll
- ocamlgraph-1.7/src/graphviz.ml
- ocamlgraph-1.7/src/graphviz.mli
- ocamlgraph-1.7/src/imperative.ml
- ocamlgraph-1.7/src/imperative.mli
- ocamlgraph-1.7/src/kruskal.ml
- ocamlgraph-1.7/src/kruskal.mli
- ocamlgraph-1.7/src/mcs_m.ml
- ocamlgraph-1.7/src/mcs_m.mli
- ocamlgraph-1.7/src/md.ml
- ocamlgraph-1.7/src/md.mli
- ocamlgraph-1.7/src/minsep.ml
- ocamlgraph-1.7/src/minsep.mli
- ocamlgraph-1.7/src/oper.ml
- ocamlgraph-1.7/src/oper.mli
- ocamlgraph-1.7/src/pack.ml
- ocamlgraph-1.7/src/pack.mli
- ocamlgraph-1.7/src/path.ml
- ocamlgraph-1.7/src/path.mli
- ocamlgraph-1.7/src/persistent.ml
- ocamlgraph-1.7/src/persistent.mli
- ocamlgraph-1.7/src/rand.ml
- ocamlgraph-1.7/src/rand.mli
- ocamlgraph-1.7/src/sig.mli
- ocamlgraph-1.7/src/sig_pack.mli
- ocamlgraph-1.7/src/strat.ml
- ocamlgraph-1.7/src/strat.mli
- ocamlgraph-1.7/src/topological.ml
- ocamlgraph-1.7/src/topological.mli
- ocamlgraph-1.7/src/traverse.ml
- ocamlgraph-1.7/src/traverse.mli
- ocamlgraph-1.7/src/util.ml
- ocamlgraph-1.7/src/util.mli
- ocamlgraph-1.7/src/version.ml
- ocamlgraph-1.7/lib/
- ocamlgraph-1.7/lib/bitv.ml
- ocamlgraph-1.7/lib/bitv.mli
- ocamlgraph-1.7/lib/heap.ml
- ocamlgraph-1.7/lib/heap.mli
- ocamlgraph-1.7/lib/unionfind.ml
- ocamlgraph-1.7/lib/unionfind.mli
- ocamlgraph-1.7/Makefile.in
- ocamlgraph-1.7/configure
- ocamlgraph-1.7/configure.in
- ocamlgraph-1.7/META.in
- ocamlgraph-1.7/.depend
- ocamlgraph-1.7/editor/
- ocamlgraph-1.7/editor/ed_display.ml
- ocamlgraph-1.7/editor/ed_draw.ml
- ocamlgraph-1.7/editor/ed_graph.ml
- ocamlgraph-1.7/editor/ed_hyper.ml
- ocamlgraph-1.7/editor/ed_main.ml
- ocamlgraph-1.7/editor/Makefile
- ocamlgraph-1.7/editor/tests/
- ocamlgraph-1.7/editor/tests/dep_ed.dot
- ocamlgraph-1.7/editor/tests/dep_why.dot
- ocamlgraph-1.7/editor/tests/fsm.dot
- ocamlgraph-1.7/editor/tests/parcours.dot
- ocamlgraph-1.7/editor/tests/softmaint.dot
- ocamlgraph-1.7/editor/tests/transparency.dot
- ocamlgraph-1.7/editor/tests/twopi2.dot
- ocamlgraph-1.7/editor/tests/unix.dot
- ocamlgraph-1.7/editor/tests/world.dot
- ocamlgraph-1.7/editor/tests/de_bruijn4.gml
- ocamlgraph-1.7/editor/tests/divisors12.gml
- ocamlgraph-1.7/editor/tests/full10.gml
- ocamlgraph-1.7/editor/tests/full20.gml
- ocamlgraph-1.7/editor/tests/full30.gml
- ocamlgraph-1.7/editor/tests/full50.gml
- ocamlgraph-1.7/editor/tests/rand_100_10.gml
- ocamlgraph-1.7/editor/tests/rand_100_300.gml
- ocamlgraph-1.7/editor/tests/rand_10_10.gml
- ocamlgraph-1.7/editor/tests/rand_10_40.gml
- ocamlgraph-1.7/editor/tests/rand_50_300.gml
- ocamlgraph-1.7/editor/tests/ring_100.gml
- ocamlgraph-1.7/editor/tests/test.gml
- ocamlgraph-1.7/editor/tests/test2,1_2.gml
- ocamlgraph-1.7/editor/tests/test2,1_3.gml
- ocamlgraph-1.7/editor/tests/test2,1_3tot.gml
- ocamlgraph-1.7/editor/tests/test2_2.gml
- ocamlgraph-1.7/view_graph/
- ocamlgraph-1.7/view_graph/viewGraph_core.ml
- ocamlgraph-1.7/view_graph/viewGraph_select.ml
- ocamlgraph-1.7/view_graph/viewGraph_test.ml
- ocamlgraph-1.7/view_graph/viewGraph_utils.ml
- ocamlgraph-1.7/view_graph/viewGraph_core.mli
- ocamlgraph-1.7/view_graph/viewGraph_select.mli
- ocamlgraph-1.7/view_graph/viewGraph_utils.mli
- ocamlgraph-1.7/view_graph/README
- ocamlgraph-1.7/view_graph/Makefile
- ocamlgraph-1.7/dgraph/
- ocamlgraph-1.7/dgraph/dGraphContainer.ml
- ocamlgraph-1.7/dgraph/dGraphMake.ml
- ocamlgraph-1.7/dgraph/dGraphModel.ml
- ocamlgraph-1.7/dgraph/dGraphRandModel.ml
- ocamlgraph-1.7/dgraph/dGraphSubTree.ml
- ocamlgraph-1.7/dgraph/dGraphTreeLayout.ml
- ocamlgraph-1.7/dgraph/dGraphTreeModel.ml
- ocamlgraph-1.7/dgraph/dGraphView.ml
- ocamlgraph-1.7/dgraph/dGraphViewItem.ml
- ocamlgraph-1.7/dgraph/dGraphViewer.ml
- ocamlgraph-1.7/dgraph/xDot.ml
- ocamlgraph-1.7/dgraph/xDotDraw.ml
- ocamlgraph-1.7/dgraph/dGraphContainer.mli
- ocamlgraph-1.7/dgraph/dGraphModel.mli
- ocamlgraph-1.7/dgraph/dGraphRandModel.mli
- ocamlgraph-1.7/dgraph/dGraphSubTree.mli
- ocamlgraph-1.7/dgraph/dGraphTreeLayout.mli
- ocamlgraph-1.7/dgraph/dGraphTreeModel.mli
- ocamlgraph-1.7/dgraph/dGraphView.mli
- ocamlgraph-1.7/dgraph/dGraphViewItem.mli
- ocamlgraph-1.7/dgraph/xDot.mli
- ocamlgraph-1.7/dgraph/xDotDraw.mli
- ocamlgraph-1.7/examples/
- ocamlgraph-1.7/examples/color.ml
- ocamlgraph-1.7/examples/demo.ml
- ocamlgraph-1.7/examples/demo_planar.ml
- ocamlgraph-1.7/examples/sudoku.ml
- ocamlgraph-1.7/tests/
- ocamlgraph-1.7/tests/bench.ml
- ocamlgraph-1.7/tests/check.ml
- ocamlgraph-1.7/tests/dot.ml
- ocamlgraph-1.7/tests/strat.ml
- ocamlgraph-1.7/tests/test.ml
- ocamlgraph-1.7/README
- ocamlgraph-1.7/FAQ
- ocamlgraph-1.7/CREDITS
- ocamlgraph-1.7/INSTALL
- ocamlgraph-1.7/COPYING
- ocamlgraph-1.7/LICENSE
- ocamlgraph-1.7/CHANGES
- cd ../ocamlgraph-1.7 && patch -p1 < ../ocamlgraph-safe-string.patch
- patching file lib/bitv.ml
- Hunk #1 succeeded at 459 with fuzz 2 (offset 10 lines).
- cd ../ocamlgraph-1.7 && ./configure
- checking for ocamlc... ocamlc
- ocaml version is 4.10.2
- ocaml library path is /home/opam/.opam/4.10/lib/ocaml
- checking for ocamlopt... ocamlopt
- checking ocamlopt version... ok
- checking for ocamlc.opt... ocamlc.opt
- checking ocamlc.opt version... ok
- checking for ocamlopt.opt... ocamlopt.opt
- checking ocamlc.opt version... ok
- checking for ocamldep... ocamldep
- checking for ocamllex... ocamllex
- checking for ocamllex.opt... ocamllex.opt
- checking for ocamlyacc... ocamlyacc
- checking for ocamldoc... ocamldoc
- checking for ocamldoc.opt... ocamldoc.opt
- checking for ocamlweb... true
- checking for ocamlfind... no
- checking for /home/opam/.opam/4.10/lib/ocaml/lablgtk2/lablgtk.cmxa... no
- checking Win32 platform... no
- configure: WARNING: lablgnomecanvas not found: the graph editor and view_graph will not be compiled
- configure: creating ./config.status
- config.status: creating Makefile
- cd ../ocamlgraph-1.7 && \
- make OCAMLOPT='ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib' graph.cmxa
- make[2]: Entering directory '/home/opam/.opam/4.10/.opam-switch/build/ott.0.27/ocamlgraph-1.7'
- sed -e s/VERSION/1.7/ -e s/CMA/graph.cma/ -e s/CMXA/graph.cmxa/ \
- 	META.in > META
- rm -f src/version.ml
- echo "let version = \""1.7"\"" > src/version.ml
- echo "let date = \""`date`"\"" >> src/version.ml
- rm -f .depend
- ocamldep -slash -I src -I lib -I editor -I view_graph -I dgraph\
- 	lib/*.ml lib/*.mli \
- 	src/*.ml src/*.mli \
- 	editor/*.mli editor/*.ml \
- 	view_graph/*.mli view_graph/*.ml \
- 	dgraph/*.mli dgraph/*.ml > .depend
- ocamlc.opt -c -I src -I lib -g -dtypes src/sig.mli
- ocamlc.opt -c -I src -I lib -g -dtypes src/sig_pack.mli
- ocamlc.opt -c -I src -I lib -g -dtypes src/dot_ast.mli
- ocamlc.opt -c -I src -I lib -g -dtypes lib/unionfind.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph lib/unionfind.ml
- ocamlc.opt -c -I src -I lib -g -dtypes lib/heap.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph lib/heap.ml
- File "lib/heap.ml", line 54, characters 13-25:
- 54 |     let d' = Array.create n' d.(0) in
-                   ^^^^^^^^^^^^
- Alert deprecated: Stdlib.Array.create
- Use Array.make instead.
- File "lib/heap.ml", line 61, characters 16-28:
- 61 |       h.data <- Array.create (- h.size) x; h.size <- 0
-                      ^^^^^^^^^^^^
- Alert deprecated: Stdlib.Array.create
- Use Array.make instead.
- ocamlc.opt -c -I src -I lib -g -dtypes lib/bitv.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph lib/bitv.ml
- File "lib/bitv.ml", line 51, characters 15-27:
- 51 | let low_mask = Array.create (succ bpi) 0
-                     ^^^^^^^^^^^^
- Alert deprecated: Stdlib.Array.create
- Use Array.make instead.
- File "lib/bitv.ml", line 68, characters 25-37:
- 68 |     { length = n; bits = Array.create (n / bpi) initv }
-                               ^^^^^^^^^^^^
- Alert deprecated: Stdlib.Array.create
- Use Array.make instead.
- File "lib/bitv.ml", line 71, characters 12-24:
- 71 |     let b = Array.create (succ s) initv in
-                  ^^^^^^^^^^^^
- Alert deprecated: Stdlib.Array.create
- Use Array.make instead.
- File "lib/bitv.ml", line 113, characters 11-13:
- 113 |   if n < 0 or n >= v.length then invalid_arg "Bitv.get";
-                  ^^
- Alert deprecated: Stdlib.or
- Use (||) instead.
- File "lib/bitv.ml", line 118, characters 11-13:
- 118 |   if n < 0 or n >= v.length then invalid_arg "Bitv.set";
-                  ^^
- Alert deprecated: Stdlib.or
- Use (||) instead.
- File "lib/bitv.ml", line 205, characters 13-15:
- 205 |   if len < 0 or ofs1 < 0 or ofs1 + len > v1.length
-                    ^^
- Alert deprecated: Stdlib.or
- Use (||) instead.
- File "lib/bitv.ml", line 205, characters 25-27:
- 205 |   if len < 0 or ofs1 < 0 or ofs1 + len > v1.length
-                                ^^
- Alert deprecated: Stdlib.or
- Use (||) instead.
- File "lib/bitv.ml", line 206, characters 13-15:
- 206 |              or ofs2 < 0 or ofs2 + len > v2.length
-                    ^^
- Alert deprecated: Stdlib.or
- Use (||) instead.
- File "lib/bitv.ml", line 206, characters 25-27:
- 206 |              or ofs2 < 0 or ofs2 + len > v2.length
-                                ^^
- Alert deprecated: Stdlib.or
- Use (||) instead.
- File "lib/bitv.ml", line 214, characters 13-15:
- 214 |   if ofs < 0 or len < 0 or ofs + len > v.length then invalid_arg "Bitv.sub";
-                    ^^
- Alert deprecated: Stdlib.or
- Use (||) instead.
- File "lib/bitv.ml", line 214, characters 24-26:
- 214 |   if ofs < 0 or len < 0 or ofs + len > v.length then invalid_arg "Bitv.sub";
-                               ^^
- Alert deprecated: Stdlib.or
- Use (||) instead.
- File "lib/bitv.ml", line 289, characters 13-15:
- 289 |   if ofs < 0 or len < 0 or ofs + len > v.length then invalid_arg "Bitv.fill";
-                    ^^
- Alert deprecated: Stdlib.or
- Use (||) instead.
- File "lib/bitv.ml", line 289, characters 24-26:
- 289 |   if ofs < 0 or len < 0 or ofs + len > v.length then invalid_arg "Bitv.fill";
-                               ^^
- Alert deprecated: Stdlib.or
- Use (||) instead.
- File "lib/bitv.ml", line 368, characters 10-22:
- 368 |   let a = Array.create n 0 in
-                 ^^^^^^^^^^^^
- Alert deprecated: Stdlib.Array.create
- Use Array.make instead.
- File "lib/bitv.ml", line 380, characters 10-22:
- 380 |   let a = Array.create n 0 in
-                 ^^^^^^^^^^^^
- Alert deprecated: Stdlib.Array.create
- Use Array.make instead.
- File "lib/bitv.ml", line 392, characters 10-22:
- 392 |   let a = Array.create n 0 in
-                 ^^^^^^^^^^^^
- Alert deprecated: Stdlib.Array.create
- Use Array.make instead.
- File "lib/bitv.ml", line 401, characters 10-22:
- 401 |   let a = Array.create n 0 in
-                 ^^^^^^^^^^^^
- Alert deprecated: Stdlib.Array.create
- Use Array.make instead.
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/version.ml
- ocamlc.opt -c -I src -I lib -g -dtypes src/util.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/util.ml
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/blocks.ml
- ocamlc.opt -c -I src -I lib -g -dtypes src/persistent.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/persistent.ml
- File "src/persistent.ml", line 52, characters 20-38:
- 52 |   let compare x y = Pervasives.compare x.tag y.tag
-                          ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "src/persistent.ml", line 145, characters 10-25:
- 145 | 	  size = Pervasives.succ g.size }
-                 ^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "src/persistent.ml", line 158, characters 21-36:
- 158 | 	{ edges = e; size = Pervasives.pred g.size }
-                            ^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "src/persistent.ml", line 178, characters 10-25:
- 178 | 	  size = Pervasives.succ g.size }
-                 ^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "src/persistent.ml", line 197, characters 10-25:
- 197 | 	  size = Pervasives.pred g.size }
-                 ^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- ocamlc.opt -c -I src -I lib -g -dtypes src/imperative.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/imperative.ml
- File "src/imperative.ml", line 68, characters 20-38:
- 68 |   let compare x y = Pervasives.compare x.tag y.tag
-                          ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "src/imperative.ml", line 169, characters 11-26:
- 169 | 	g.size <- Pervasives.succ g.size;
-                  ^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "src/imperative.ml", line 185, characters 11-26:
- 185 | 	g.size <- Pervasives.pred g.size
-                  ^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "src/imperative.ml", line 206, characters 11-26:
- 206 | 	g.size <- Pervasives.succ g.size;
-                  ^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "src/imperative.ml", line 227, characters 11-26:
- 227 | 	g.size <- Pervasives.pred g.size
-                  ^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "src/imperative.ml", line 371, characters 36-54:
- 371 |       let compare : t -> t -> int = Pervasives.compare
-                                           ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "src/imperative.ml", line 381, characters 36-54:
- 381 |       let compare : t -> t -> int = Pervasives.compare
-                                           ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- ocamlc.opt -c -I src -I lib -g -dtypes src/delaunay.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/delaunay.ml
- File "src/delaunay.ml", line 260, characters 19-31:
- 260 |     let seen_arc = Array.create n false in
-                          ^^^^^^^^^^^^
- Alert deprecated: Stdlib.Array.create
- Use Array.make instead.
- ocamlc.opt -c -I src -I lib -g -dtypes src/builder.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/builder.ml
- ocamlc.opt -c -I src -I lib -g -dtypes src/classic.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/classic.ml
- ocamlc.opt -c -I src -I lib -g -dtypes src/rand.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/rand.ml
- ocamlc.opt -c -I src -I lib -g -dtypes src/oper.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/oper.ml
- ocamlc.opt -c -I src -I lib -g -dtypes src/path.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/path.ml
- ocamlc.opt -c -I src -I lib -g -dtypes src/traverse.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/traverse.ml
- ocamlc.opt -c -I src -I lib -g -dtypes src/coloring.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/coloring.ml
- ocamlc.opt -c -I src -I lib -g -dtypes src/topological.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/topological.ml
- ocamlc.opt -c -I src -I lib -g -dtypes src/components.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/components.ml
- ocamlc.opt -c -I src -I lib -g -dtypes src/kruskal.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/kruskal.ml
- ocamlc.opt -c -I src -I lib -g -dtypes src/flow.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/flow.ml
- File "src/flow.ml", line 53, characters 54-56:
- 53 |   let fold_booleen f = List.fold_left (fun r x->(f x) or r) false
-                                                            ^^
- Alert deprecated: Stdlib.or
- Use (||) instead.
- File "src/flow.ml", line 137, characters 6-8:
- 137 |       or G.fold_pred_e (fun e r->pousser g e l or r) g x false
-             ^^
- Alert deprecated: Stdlib.or
- Use (||) instead.
- File "src/flow.ml", line 136, characters 44-46:
- 136 |       G.fold_succ_e (fun e r->pousser g e l or r) g x false
-                                                   ^^
- Alert deprecated: Stdlib.or
- Use (||) instead.
- File "src/flow.ml", line 137, characters 47-49:
- 137 |       or G.fold_pred_e (fun e r->pousser g e l or r) g x false
-                                                      ^^
- Alert deprecated: Stdlib.or
- Use (||) instead.
- File "src/flow.ml", line 141, characters 40-42:
- 141 |       (fold_booleen (elever g p) !todo) or 
-                                               ^^
- Alert deprecated: Stdlib.or
- Use (||) instead.
- ocamlc.opt -c -I src -I lib -g -dtypes src/graphviz.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/graphviz.ml
- File "src/graphviz.ml", line 27, characters 5-15:
- 27 | open Pervasives (* for compatibility with ocaml 3.12.0+dev17
-           ^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- ocamlc.opt -c -I src -I lib -g -dtypes src/gml.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/gml.ml
- File "src/gml.ml", line 418, characters 27-39:
- 418 |   lexbuf.Lexing.lex_mem <- Array.create 2 (-1) ;   __ocaml_lex_file_rec lexbuf 0
-                                  ^^^^^^^^^^^^
- Alert deprecated: Stdlib.Array.create
- Use Array.make instead.
- File "src/gml.ml", line 455, characters 27-39:
- 455 |   lexbuf.Lexing.lex_mem <- Array.create 2 (-1) ;   __ocaml_lex_value_list_rec lexbuf 7
-                                  ^^^^^^^^^^^^
- Alert deprecated: Stdlib.Array.create
- Use Array.make instead.
- ocamlc.opt -c -I src -I lib -g -dtypes src/dot_parser.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/dot_parser.ml
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/dot_lexer.ml
- File "src/dot_lexer.mll", line 39, characters 21-37:
- Alert deprecated: Stdlib.String.lowercase
- Use String.lowercase_ascii instead.
- ocamlc.opt -c -I src -I lib -g -dtypes src/dot.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/dot.ml
- File "src/dot.ml", line 61, characters 41-59:
- 61 |            let compare : t -> t -> int = Pervasives.compare
-                                               ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- ocamlc.opt -c -I src -I lib -g -dtypes src/pack.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/pack.ml
- File "src/pack.ml", line 51, characters 34-52:
- 51 |     let compare : t -> t -> int = Pervasives.compare
-                                        ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "src/pack.ml", line 64, characters 34-52:
- 64 |     let compare : t -> t -> int = Pervasives.compare
-                                        ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "src/pack.ml", line 89, characters 34-52:
- 89 |     let compare : t -> t -> int = Pervasives.compare
-                                        ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "src/pack.ml", line 170, characters 32-50:
- 170 |   let compare : t -> t -> int = Pervasives.compare
-                                       ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- ocamlc.opt -c -I src -I lib -g -dtypes src/gmap.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/gmap.ml
- ocamlc.opt -c -I src -I lib -g -dtypes src/minsep.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/minsep.ml
- ocamlc.opt -c -I src -I lib -g -dtypes src/cliquetree.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/cliquetree.ml
- File "src/cliquetree.ml", line 110, characters 39-57:
- 110 |          let compare : t -> t -> int = Pervasives.compare
-                                              ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "src/cliquetree.ml", line 120, characters 40-58:
- 120 |     let compare (x, _ : t) (y, _ : t) = Pervasives.compare x y
-                                               ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "src/cliquetree.ml", line 171, characters 3-21:
- 171 | 	 (Pervasives.compare : int -> int -> int) (number y) (number x))
-          ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- ocamlc.opt -c -I src -I lib -g -dtypes src/mcs_m.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/mcs_m.ml
- ocamlc.opt -c -I src -I lib -g -dtypes src/md.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/md.ml
- ocamlc.opt -c -I src -I lib -g -dtypes src/strat.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -c -I src -I lib -for-pack Graph src/strat.ml
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -I src -I lib -pack -o graph.cmx src/sig.cmi src/sig_pack.cmi src/dot_ast.cmi lib/unionfind.cmx lib/heap.cmx lib/bitv.cmx src/version.cmx src/util.cmx src/blocks.cmx src/persistent.cmx src/imperative.cmx src/delaunay.cmx src/builder.cmx src/classic.cmx src/rand.cmx src/oper.cmx src/path.cmx src/traverse.cmx src/coloring.cmx src/topological.cmx src/components.cmx src/kruskal.cmx src/flow.cmx src/graphviz.cmx src/gml.cmx src/dot_parser.cmx src/dot_lexer.cmx src/dot.cmx src/pack.cmx src/gmap.cmx src/minsep.cmx src/cliquetree.cmx src/mcs_m.cmx src/md.cmx src/strat.cmx
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I src -I lib -I src -I lib -a -o graph.cmxa graph.cmx
- make[2]: Leaving directory '/home/opam/.opam/4.10/.opam-switch/build/ott.0.27/ocamlgraph-1.7'
- make opt
- make[2]: Entering directory '/home/opam/.opam/4.10/.opam-switch/build/ott.0.27/src'
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I ../ocamlgraph-1.7 -c location.ml
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I ../ocamlgraph-1.7 -c types.ml
- File "types.ml", line 484, characters 67-85:
- 484 | module NtrSet = Set.Make(struct type t = nontermroot let compare = Pervasives.compare end);;
-                                                                          ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "types.ml", line 490, characters 83-101:
- 490 | module NtrPairSet = Set.Make(struct type t = nontermroot*nontermroot let compare = Pervasives.compare end);;
-                                                                                          ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "types.ml", line 497, characters 87-105:
- 497 | module NtSet = Set.Make(struct type t = nontermroot * nonterm * prod_env let compare = Pervasives.compare end);;
-                                                                                              ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "types.ml", line 504, characters 93-111:
- 504 | module NtsubSet = Set.Make(struct type t = nontermroot * nontermroot * nonterm let compare = Pervasives.compare end);;
-                                                                                                    ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "types.ml", line 510, characters 68-86:
- 510 | module MvrSet = Set.Make(struct type t = metavarroot  let compare = Pervasives.compare end);;
-                                                                           ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "types.ml", line 517, characters 88-106:
- 517 | module MvSet = Set.Make(struct type t =  metavarroot * metavar * prod_env let compare = Pervasives.compare end);;
-                                                                                               ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I ../ocamlgraph-1.7 -c auxl.ml
- File "auxl.ml", lines 396-403, characters 7-19:
- 396 | .......( match hse with
- 397 | 	      | Hom_index _ | Hom_terminal _ -> []
- 398 | 	      | Hom_string s -> 
- 399 | 		  let strs = Str.split (Str.regexp "[ \t]+") s in
- 400 | 		  let ntrs_hom = List.filter (fun st -> List.mem st defined_ntrs) strs in
- 401 | 		  if promote 
- 402 | 		  then List.map (promote_ntr xd) ntrs_hom
- 403 | 		  else ntrs_hom ).
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Hom_ln_free_index (_, _)
- File "auxl.ml", lines 458-462, characters 7-59:
- 458 | .......( match hse with
- 459 | 	      | Hom_index _ | Hom_terminal _ -> []
- 460 | 	      | Hom_string s -> 
- 461 | 		  let strs = Str.split (Str.regexp "[ \t]+") s in
- 462 | 		  List.filter (fun st -> List.mem st defined_mvrs) strs ).
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Hom_ln_free_index (_, _)
- File "auxl.ml", lines 791-795, characters 2-61:
- 791 | ..match m with
- 792 |   | Coq _ | Hol _ | Lem _ | Isa _ | Caml _ -> "(** "^s^" *)\n"
- 793 |   | Twf _ -> "%%% "^s^" %%%\n\n"
- 794 |   | Tex _ -> "% "^s^"\n"
- 795 |   | Menhir _ | Lex _ | Ascii _ -> errorm m "big_line_comment"
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "auxl.ml", line 1492, characters 47-64:
- 1492 |   let map_prod_names = List.map (fun pn -> (pn,String.capitalize pn)) prod_name_list in
-                                                       ^^^^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.String.capitalize
- Use String.capitalize_ascii instead.
- File "auxl.ml", line 1502, characters 47-66:
- 1502 |   let map_prod_names = List.map (fun pn -> (pn,String.uncapitalize pn)) prod_name_list in
-                                                       ^^^^^^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.String.uncapitalize
- Use String.uncapitalize_ascii instead.
- File "auxl.ml", line 1511, characters 51-70:
- 1511 |   let map_nontermroots = List.map (fun ntr -> (ntr,String.uncapitalize ntr)) nontermroots_list in
-                                                           ^^^^^^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.String.uncapitalize
- Use String.uncapitalize_ascii instead.
- File "auxl.ml", line 1520, characters 51-70:
- 1520 |   let map_metavarroots = List.map (fun mvr -> (mvr,String.uncapitalize mvr)) metavarroots_list in
-                                                           ^^^^^^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.String.uncapitalize
- Use String.uncapitalize_ascii instead.
- File "auxl.ml", line 1544, characters 19-36:
- 1544 |     st_prod_name = String.capitalize stnb.st_prod_name;
-                           ^^^^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.String.capitalize
- Use String.capitalize_ascii instead.
- File "auxl.ml", lines 1569-1578, characters 2-68:
- 1569 | ..match m with 
- 1570 |   | Isa _ -> "True" 
- 1571 |   | Coq co ->
- 1572 |       if co.coq_expand_lists || in_prop  
- 1573 |       then "True"     
- 1574 |       else "true"
- 1575 |   | Hol _ -> "T" 
- 1576 |   | Caml _ -> "true" 
- 1577 |   | Lem _ -> "true" 
- 1578 |   | Ascii _ | Tex _ | Twf _ | Lex _ | Menhir _ -> errorm m "pp_true"
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "auxl.ml", lines 1581-1590, characters 2-69:
- 1581 | ..match m with 
- 1582 |   | Isa _ -> "False" 
- 1583 |   | Coq co ->
- 1584 |       if co.coq_expand_lists || in_prop 
- 1585 |       then "False"     
- 1586 |       else "false"
- 1587 |   | Hol _ -> "F" 
- 1588 |   | Caml _ -> "false"
- 1589 |   | Lem _ -> "false"
- 1590 |   | Ascii _ | Tex _ | Twf _ | Lex _ | Menhir _ -> errorm m "pp_false"
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "auxl.ml", lines 1593-1602, characters 2-67:
- 1593 | ..match m with
- 1594 |   | Isa _ -> " & " 
- 1595 |   | Caml _ -> " && " 
- 1596 |   | Lem _ -> " && " 
- 1597 |   | Coq co ->
- 1598 |       if co.coq_expand_lists || in_prop
- 1599 |       then " /\\ "     
- 1600 |       else " && "
- 1601 |   | Hol _ -> " /\\ "
- 1602 |   | Ascii _ | Tex _ | Twf _ | Lex _ | Menhir _ -> errorm m "pp_and"
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "auxl.ml", lines 1605-1614, characters 2-66:
- 1605 | ..match m with 
- 1606 |   | Isa _ -> " | " 
- 1607 |   | Coq co ->
- 1608 |       if co.coq_expand_lists || in_prop 
- 1609 |       then " \\/ "     
- 1610 |       else " || "
- 1611 |   | Hol _ -> " \\/ " 
- 1612 |   | Caml _ -> " || "
- 1613 |   | Lem _ -> " || "
- 1614 |   | Ascii _ | Tex _ | Twf _ | Lex _ | Menhir _ -> errorm m "pp_or"
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "auxl.ml", lines 1622-1657, characters 2-97:
- 1622 | ..match m with
- 1623 |   | Coq _ ->
- 1624 |       ( match l with
- 1625 |       | [] -> "nil"
- 1626 |       | x::[] -> "("^x^")"
- ...
- 1654 | 	  ^ ( String.concat " <- " 
- 1655 | 	      (List.map2 (fun s nl -> s ^ " " ^ nl) l list_nl) )
- 1656 | 	  ^ final_append )
- 1657 |   | Caml _ | Tex _ | Ascii _ | Hol _ | Lem _ | Isa _ | Lex _ | Menhir _ -> raise ThisCannotHappen
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "auxl.ml", lines 1809-1824, characters 4-42:
- 1809 | ....( match stre with 
- 1810 |     | Struct_md mvr ->  "metavar def: "^mvr
- 1811 |     | Struct_rs ntrs -> "rule def: "^(String.concat " " ntrs)
- 1812 |     | Struct_srs xs -> "subrule def: "^
- 1813 | 	(String.concat " " 
- ...
- 1821 |     | Struct_axs xs -> "aux def: "^
- 1822 |         (String.concat " " xs)
- 1823 |     | Struct_fun_or_defnclass s -> "fundefn_class def: "^s
- 1824 |     | Struct_embed (_,h,_) -> "embed: "^h)
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Struct_crs _
- ocamlc -g -dtypes   -c location.ml
- ocamlc -g -dtypes   -c types.ml
- File "types.ml", line 484, characters 67-85:
- 484 | module NtrSet = Set.Make(struct type t = nontermroot let compare = Pervasives.compare end);;
-                                                                          ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "types.ml", line 490, characters 83-101:
- 490 | module NtrPairSet = Set.Make(struct type t = nontermroot*nontermroot let compare = Pervasives.compare end);;
-                                                                                          ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "types.ml", line 497, characters 87-105:
- 497 | module NtSet = Set.Make(struct type t = nontermroot * nonterm * prod_env let compare = Pervasives.compare end);;
-                                                                                              ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "types.ml", line 504, characters 93-111:
- 504 | module NtsubSet = Set.Make(struct type t = nontermroot * nontermroot * nonterm let compare = Pervasives.compare end);;
-                                                                                                    ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "types.ml", line 510, characters 68-86:
- 510 | module MvrSet = Set.Make(struct type t = metavarroot  let compare = Pervasives.compare end);;
-                                                                           ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "types.ml", line 517, characters 88-106:
- 517 | module MvSet = Set.Make(struct type t =  metavarroot * metavar * prod_env let compare = Pervasives.compare end);;
-                                                                                               ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- ocamlc -g -dtypes   -I ../ocamlgraph-1.7 -c merge.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I ../ocamlgraph-1.7 -c merge.ml
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I ../ocamlgraph-1.7 -c global_option.ml
- ocamlc -g -dtypes   -I ../ocamlgraph-1.7 -c grammar_parser.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I ../ocamlgraph-1.7 -c grammar_parser.ml
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I ../ocamlgraph-1.7 -c grammar_lexer.ml
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I ../ocamlgraph-1.7 -c version.ml
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I ../ocamlgraph-1.7 -c grammar_pp.ml
- File "grammar_pp.ml", lines 86-90, characters 2-26:
- 86 | ..match m with
- 87 |   | Ascii _ 
- 88 |   | Tex _ -> Printf.sprintf "%% %s\n" s
- 89 |   | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _  ->  Printf.sprintf "(* %s *)\n" s
- 90 |   | Lex _ | Menhir _ -> ""..
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", lines 874-888, characters 2-28:
- 874 | ..match m with
- 875 |   | Ascii ao -> 
- 876 |       ( match n with 
- 877 |       | 0 -> pp_DOTDOT 
- 878 |       | 1 -> pp_DOTDOTDOT 
- ...
- 885 |       | 2 -> pp_tex_DOTDOTDOTDOT 
- 886 |       | _ -> raise ThisCannotHappen )
- 887 |   | Caml _ | Hol _ | Lem _ | Isa _ | Coq _ | Twf _ | Lex _ | Menhir _ -> 
- 888 |       raise ThisCannotHappen
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", lines 891-898, characters 2-37:
- 891 | ..match m with
- 892 |   | Ascii ao -> col_cyan ao ("(*"^s^"*)")
- 893 |   | Caml _ | Coq _ | Isa _ | Hol _ | Lem _ | Lex _ | Menhir _ -> "(*"^s^"*)"  
- 894 |   | Twf _  -> "%{"^s^"}%"  
- 895 |   | Tex _ -> 
- 896 |       let es = Auxl.pp_tex_escape s in
- 897 |       if (String.length es > 1) || (Auxl.is_alpha es) 
- 898 |       then "\\mathbf{"^es^"}" else es.................................
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", lines 901-903, characters 2-82:
- 901 | ..match m with 
- 902 |   | Ascii ao -> quote_ident s
- 903 |   | Tex _ | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> s
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", lines 906-909, characters 2-95:
- 906 | ..match m with
- 907 |   | Ascii _ -> pp_BAR
- 908 |   | Tex _ -> pp_tex_BAR
- 909 |   | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", lines 927-936, characters 2-26:
- 927 | ..match m with 
- 928 |   | Ascii ao -> col_green ao tm
- 929 |   | Tex _ -> pp_tex_terminal m xd tm
- 930 |   | Coq _ -> tm
- 931 |   | Isa _ -> pp_isa_terminal m xd tm
- 932 |   | Hol _ -> tm
- 933 |   | Lem _ -> tm
- 934 |   | Twf _ -> tm
- 935 |   | Caml _ -> "_" (* tm *)
- 936 |   | Lex _ | Menhir _ -> tm
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", line 972, characters 19-36:
- 972 |   | Twf _,false -> String.capitalize s
-                          ^^^^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.String.capitalize
- Use String.capitalize_ascii instead.
- File "grammar_pp.ml", lines 1107-1173, characters 10-101:
- 1107 | ..........match m with
- 1108 |           | Isa _ -> 
- 1109 |               "((%"^de1i.de1_pattern^" . "^pp_nt_or_mv_with_sie m xd ((Si_var ("_",0))::sie) (ntmvr,suff)^")"
- 1110 |               ^ " (List.nth " ^ de1i.de1_compound_id ^ " " 
- 1111 |               ^ "(" ^ pp_plain_suffix_item suffi 
- ...
- 1170 | 	      else "(match " ^ hyp_var ^ " with " ^ de1i.de1_pattern ^ " => " ^ proj_arg ^" end)" )
- 1171 |           | Ascii _ | Tex _ -> raise ThisCannotHappen
- 1172 |           | Twf _ -> raise TwelfNotImplemented
- 1173 |           | Caml _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_symterm for proper symterms not supported"
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", line 1363, characters 22-39:
- 1363 |   | Caml _ | Lem _ -> String.capitalize (pp_maybe_quote_ident m xd pn)
-                              ^^^^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.String.capitalize
- Use String.capitalize_ascii instead.
- File "grammar_pp.ml", lines 1424-1438, characters 2-49:
- 1424 | ..match (m,hn) with 
- 1425 |   | (Ascii ao, _) -> 
- 1426 |       pp_DOUBLELEFTBRACE ^ " "
- 1427 |       ^ (pp_hom_name m xd hn) ^ " "
- 1428 |       ^ (pp_hom_spec m xd hs) ^ " "
- ...
- 1435 | (*   | (Hol ho, "hol") -> (pp_hom_spec m xd hs)^"\n\n"  *)
- 1436 | (*                        (\* raise ThisCannotHappen *\) *)
- 1437 |   | (Coq _, _) | (Isa _, _) | (Hol _,_) | (Lem _,_) | (Twf _,_) | (Caml _,_) | (Lex _,_) | (Menhir _, _) -> ""
- 1438 |   | (Tex _, _) -> Auxl.errorm m "pp_homomorphism"
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Rdx _, _)
- File "grammar_pp.ml", lines 1441-1445, characters 2-95:
- 1441 | ..match m with 
- 1442 |   | Ascii ao -> 
- 1443 |       String.concat " " (List.map (pp_homomorphism m xd) homs)
- 1444 |   | Tex xo -> raise ThisCannotHappen
- 1445 |   | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", lines 1453-1481, characters 2-62:
- 1453 | ..match m with 
- 1454 |   | Ascii ao -> 
- 1455 |       ( match hse with
- 1456 |       | Hom_string s ->  s
- 1457 |       | Hom_index i -> pp_DOUBLELEFTBRACKET^string_of_int i^pp_DOUBLERIGHTBRACKET 
- ...
- 1478 |       | Hom_string s -> s
- 1479 |       | Hom_terminal s -> s
- 1480 |       | Hom_index i -> "UNIMPLEMENTED[Hom_index"^string_of_int i^"]"
- 1481 |       | Hom_ln_free_index _ -> Auxl.errorm m "pp_hom_spec el")
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", lines 1690-1697, characters 6-101:
- 1690 | ......( match m with 
- 1691 |       | Ascii ao -> 
- 1692 |           pp_BIND^" " ^  pp_mse_string m xd sie de mse ^ " " 
- 1693 | 	  ^ pp_IN ^ " " ^ pp_nonterm m xd nt
- 1694 |       | Tex xo -> 
- 1695 |           pp_tex_BIND ^ "\\; " ^  pp_mse_string m xd sie de mse ^ "\\; "
- 1696 | 	  ^ pp_tex_IN ^ "\\; " ^ pp_nonterm m xd nt
- 1697 |       | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen )
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", lines 1699-1702, characters 6-101:
- 1699 | ......( match m with 
- 1700 |       | Ascii ao -> pp_auxfn m xd f ^ "" ^ pp_EQ ^ "" ^ pp_mse_string m xd sie de mse
- 1701 |       | Tex xo -> pp_auxfn m xd f ^ "" ^ pp_tex_EQ ^ "" ^ pp_mse_string m xd sie de mse
- 1702 |       | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen )
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", lines 1704-1713, characters 6-101:
- 1704 | ......( match m with 
- 1705 |       | Ascii ao -> 
- 1706 |           pp_NAMES ^ "" ^ pp_LPAREN ^ "" ^ pp_mse_string m xd sie de mse ^ "" ^ pp_RPAREN 
- 1707 | 	  ^ "" ^ pp_EQ ^ "" ^ pp_NAMES ^ "" 
- 1708 | 	  ^ pp_LPAREN ^ "" ^ pp_mse_string m xd sie de mse' ^ "" ^ pp_RPAREN
- 1709 |       | Tex xo -> 
- 1710 |           pp_tex_NAMES ^ "" ^ pp_tex_LPAREN ^ "" ^ pp_mse_string m xd sie de mse 
- 1711 | 	  ^ "" ^ pp_tex_RPAREN ^ "\\," ^ pp_tex_EQ ^ "\\," ^ pp_tex_NAMES
- 1712 | 	  ^ "" ^ pp_tex_LPAREN ^ "" ^ pp_mse_string m xd sie de mse' ^ "" ^ pp_tex_RPAREN
- 1713 |       | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen )
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", lines 1715-1725, characters 6-101:
- 1715 | ......( match m with 
- 1716 |       | Ascii ao -> 
- 1717 |           pp_NAMES ^ "" ^ pp_LPAREN ^ "" ^ pp_mse_string m xd sie de mse ^ "" ^ pp_RPAREN
- 1718 | 	  ^ "" ^ pp_HASH ^ "" ^ pp_NAMES ^ "" ^ pp_LPAREN ^ "" 
- 1719 | 	  ^ pp_mse_string m xd sie de mse' ^ "" ^ pp_RPAREN
- ...
- 1722 | 	  ^ ""^pp_tex_RPAREN ^ "\\," ^ pp_tex_HASH ^ "\\,"
- 1723 | 	  ^ pp_tex_NAMES ^ "" ^ pp_tex_LPAREN ^ "" ^ pp_mse_string m xd sie de mse' 
- 1724 | 	  ^ ""^pp_tex_RPAREN
- 1725 |       | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen )
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", lines 1727-1734, characters 6-101:
- 1727 | ......( match m with 
- 1728 |       | Ascii ao -> 
- 1729 |           pp_DISTINCTNAMES ^ "" ^ pp_LPAREN ^ "" ^ pp_mse_string m xd sie de mse 
- 1730 | 	  ^ "" ^ pp_RPAREN
- 1731 |       | Tex xo -> 
- 1732 |           pp_tex_DISTINCTNAMES ^ "" ^ pp_tex_LPAREN ^ "" ^ pp_mse_string m xd sie de mse 
- 1733 | 	  ^ "" ^ pp_tex_RPAREN
- 1734 |       | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen ).
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", lines 1737-1753, characters 2-105:
- 1737 | ..match m with
- 1738 |   | Tex _ -> 
- 1739 |       (List.map (pp_bindspec m xd sie de) bs)
- 1740 | 
- 1741 | (*       ( match bs with  *)
- ...
- 1750 | (*                " $ \\\\ \n  &&&&      $ "  *)
- 1751 | (*                (List.map (pp_bindspec m xd sie de) bs))  *)
- 1752 | (* 	  ^ (\* " $ & \\ $ " ^*\) pp_tex_BIND_RIGHT_DELIM ) *)
- 1753 |   | Ascii _ | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen.
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", lines 1786-1791, characters 6-87:
- 1786 | ......( match m with
- 1787 |       | Lex _ | Menhir _ -> Auxl.errorm m "pp_mse"
- 1788 |       | Ascii _ | Tex _ -> (* "\\{" ^*)  pp_metavar_with_sie m xd sie mv (* ^ "\\}" *)
- 1789 |       | Isa _ | Hol _ | Lem _ | Caml _ -> "["^pp_metavar_with_sie m xd sie mv^"]"
- 1790 |       | Coq _ -> "(cons " ^ pp_metavar_with_sie m xd sie mv ^ " nil)" 
- 1791 |       | Twf _ -> "(natlist/cons " ^ pp_metavar_with_sie m xd sie mv ^ " natlist/nil)" )........
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", lines 1793-1798, characters 6-87:
- 1793 | ......( match m with
- 1794 |       | Lex _ | Menhir _ -> Auxl.errorm m "pp_mse"
- 1795 |       | Ascii _ | Tex _ -> (* "\\{" ^*)  pp_nonterm_with_sie m xd sie nt (* ^ "\\}" *)
- 1796 |       | Isa _ | Hol _ | Lem _ | Caml _ -> "["^pp_nonterm_with_sie m xd sie nt^"]"
- 1797 |       | Coq _ -> "(cons " ^ pp_nonterm_with_sie m xd sie nt ^ " nil)" 
- 1798 |       | Twf _ -> "(natlist/cons " ^ pp_nonterm_with_sie m xd sie nt ^ " natlist/nil)" ).........
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", lines 1847-1858, characters 6-61:
- 1847 | ......( match m with 
- 1848 |       | Lex _ | Menhir _ -> Auxl.errorm m "pp_mse"
- 1849 |       | Ascii ao -> 
- 1850 |           ( pp_auxfn m xd f ^ ""^pp_LPAREN  ^ pp_nonterm_with_sie m xd sie nt 
- 1851 | 	    ^ "" ^ pp_RPAREN ), [], []
- ...
- 1855 |       | Isa _ | Coq _ | Hol _ | Lem _ | Twf _ | Caml _ -> 
- 1856 |           let ntrp = pp_nontermroot_ty m xd (Auxl.promote_ntr xd (Auxl.primary_ntr_of_ntr xd (fst nt))) in
- 1857 | 	  ( "(" ^ Auxl.auxfn_name f ntrp ntrp ^ " " 
- 1858 |             ^ pp_nonterm_with_sie m xd sie nt^")" ), [], [] )
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", lines 1883-2139, characters 6-25:
- 1883 | ......( match m with 
- 1884 |       | Lex _ | Menhir _ -> Auxl.errorm m "pp_mse"
- 1885 |       | Ascii ao -> 
- 1886 |           pp_auxfn m xd f ^ ""^pp_LPAREN ^ "" 
- 1887 |           ^ pp_ntlist
- ...
- 2136 | 	  else
- 2137 | 	    ( "(flat_map (fun "^pat_fun^" => "^pp_body^ pat_fun_end ^ ") "
- 2138 | 	      ^ de1i.de1_compound_id
- 2139 | 	      ^ ")", [], [] )  )
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Coq _|Isa _|Rdx _)
- (However, some guarded clause may match this value.)
- File "grammar_pp.ml", lines 2144-2166, characters 6-125:
- 2144 | ......( match m with 
- 2145 |       | Lex _ | Menhir _ -> Auxl.errorm m "pp_mse"
- 2146 |       | Ascii ao -> 
- 2147 |           ( pp_mse_string m xd sie de mse ^ " " ^ pp_UNION ^ " " ^ pp_mse_string m xd sie de mse' ), [], []
- 2148 |       | Tex xo -> 
- ...
- 2163 | 	  ("(app "^s1 ^ " " ^ s2^")",
- 2164 | 	   d1 @ d2,
- 2165 | 	   f1 @ f2)
- 2166 |       | Twf _ -> ( "(append/natlist " ^ pp_mse_string m xd sie de mse ^ " " ^ pp_mse_string m xd sie de mse' ^")" ), [] , [])
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", lines 2168-2175, characters 6-8:
- 2168 | ......( match m with 
- 2169 |       | Lex _ | Menhir _ -> Auxl.errorm m "pp_mse"
- 2170 |       | Ascii ao -> pp_EMPTY, [], []
- 2171 |       | Tex xo -> pp_tex_EMPTY, [], []
- 2172 |       | Isa _ | Hol _ | Lem _ | Caml _ -> "[]", [], []
- 2173 |       | Coq _ -> "nil", [], [] 
- 2174 |       | Twf _ -> "natlist/nil", [], [] 
- 2175 |        )
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", lines 2219-2228, characters 10-105:
- 2219 | ..........( match m with 
- 2220 |           | Ascii ao -> Some (
- 2221 |               pp_LEFTBRACKET ^ " " 
- 2222 | 	      ^ String.concat " " (Auxl.option_map (pp_element m xd sie in_type) es) ^ " "
- 2223 | 	      ^ pp_RIGHTBRACKET )
- 2224 |           | Tex xo -> Some (
- 2225 |               pp_tex_LEFTBRACKET ^ " " 
- 2226 | 	      ^ String.concat " " (Auxl.option_map (pp_element m xd sie in_type) es) ^ " " 
- 2227 | 	      ^ pp_tex_RIGHTBRACKET )
- 2228 |           | Coq _ | Caml _ | Hol _ | Lem _ | Twf _ | Isa _ | Lex _ | Menhir _ -> raise ThisCannotHappen )
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", lines 2276-2286, characters 12-76:
- 2276 | ............( match m with 
- 2277 |             | Coq co -> 
- 2278 | 	        ( match pp_elements m xd sie es true false true true with
- 2279 |                 | None -> None
- 2280 |                 | Some s -> Some (None, "(option "^s^")") )
- ...
- 2283 |                 | None -> None
- 2284 |                 | Some s -> Some (None, s^ " option"))
- 2285 |             | Twf _ -> raise TwelfNotImplemented
- 2286 |             | Ascii _ | Tex _ | Lex _ | Menhir _ -> raise ThisCannotHappen )
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", line 2407, characters 8-26:
- 2407 | 		  if (Pervasives.compare mv emv = 0)
-                ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "grammar_pp.ml", line 2417, characters 8-26:
- 2417 | 		  if (Pervasives.compare nt ent = 0)
-                ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "grammar_pp.ml", line 2549, characters 25-42:
- 2549 |         | None ->  Some (String.capitalize p.prod_name ^ pp_com)
-                                 ^^^^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.String.capitalize
- Use String.capitalize_ascii instead.
- File "grammar_pp.ml", line 2550, characters 28-45:
- 2550 |         | Some s ->  Some ((String.capitalize p.prod_name) ^ " of " ^ s ^ pp_com) )
-                                    ^^^^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.String.capitalize
- Use String.capitalize_ascii instead.
- File "grammar_pp.ml", line 2556, characters 25-42:
- 2556 |         | None ->  Some (String.capitalize p.prod_name ^ pp_com)
-                                 ^^^^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.String.capitalize
- Use String.capitalize_ascii instead.
- File "grammar_pp.ml", line 2557, characters 28-45:
- 2557 |         | Some s ->  Some ((String.capitalize p.prod_name) ^ " of " ^ s ^ pp_com) )
-                                    ^^^^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.String.capitalize
- Use String.capitalize_ascii instead.
- File "grammar_pp.ml", line 2771, characters 22-23:
- 2771 |                       & match m with Isa _ | Coq _ | Hol _ | Lem _ | Caml _ -> true | _ -> false) 
-                              ^
- Alert deprecated: Stdlib.&
- Use (&&) instead.
- File "grammar_pp.ml", lines 2777-2811, characters 16-91:
- 2777 | ................( match m with 
- 2778 |                 | Isa _ -> 
- 2779 |                     "type_synonym "
- 2780 |                     ^ "\"" ^ pp_nontermroot_ty m xd ntr ^ "\" = \""
- 2781 |                     ^ pp_hom_spec m xd hs
- ...
- 2808 |                     ^ pp_nontermroot_ty m xd ntr ^ " = "
- 2809 |                     ^ pp_hom_spec m xd hs
- 2810 |                     ^ "\n\n"
- 2811 |                 | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.errorm m "int_rule_list_dep" )
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", lines 2987-3010, characters 2-16:
- 2987 | ..match m with
- 2988 |   | Ascii ao -> 
- 2989 |       String.concat "\n" (List.map (pp_metavardefn m xd) xd.xd_mds) 
- 2990 |       ^ pp_RULES^"\n"
- 2991 |       ^ pp_rule_list m xd xd.xd_rs ^ "\n" 
- ...
- 3007 |       ^ "\n"^pp_tex_END_METAVARS ^"}\n\n"  (*  ^ "\\end{array}\\]\n" *)
- 3008 |       ^ pp_rule_list m xd xd.xd_rs
- 3009 |   | Lex _ | Menhir _ ->
- 3010 |       "<<TODO>>"
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", line 3558, characters 20-37:
- 3558 | 	          | [] -> (String.capitalize promoted_pn)
-                            ^^^^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.String.capitalize
- Use String.capitalize_ascii instead.
- File "grammar_pp.ml", line 3562, characters 25-42:
- 3562 |                       ^ (String.capitalize promoted_pn)^" "
-                                 ^^^^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.String.capitalize
- Use String.capitalize_ascii instead.
- File "grammar_pp.ml", line 3569, characters 20-37:
- 3569 | 	          | [] -> (String.capitalize promoted_pn)
-                            ^^^^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.String.capitalize
- Use String.capitalize_ascii instead.
- File "grammar_pp.ml", line 3573, characters 25-42:
- 3573 |                       ^ (String.capitalize promoted_pn)^" "
-                                 ^^^^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.String.capitalize
- Use String.capitalize_ascii instead.
- File "grammar_pp.ml", lines 3711-3724, characters 10-41:
- 3711 | ..........(match m with
- 3712 |       | Ascii ao -> if ao.ppa_ugly then [col_magenta ao "[empty stlis]",TTC_dummy] else ["",TTC_dummy]
- 3713 |       | Tex _ -> ["\\,",TTC_space]
- 3714 |       | Isa _ -> ["[]",TTC_dummy]
- 3715 |       | Caml _ -> ["[]",TTC_dummy]
- ...
- 3721 |            ["nil",TTC_dummy]
- 3722 |       | Hol _ -> ["NIL",TTC_dummy]
- 3723 |       | Twf _ -> raise TwelfNotImplemented
- 3724 |       | Lex _ | Menhir _ -> assert false)
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", lines 3806-3820, characters 6-51:
- 3806 | ......(match m with
- 3807 |       | Ascii ao -> if ao.ppa_ugly then [col_magenta ao "[stli_single",TTC_dummy] @ pp_es' @ [col_magenta ao "stli_single]",TTC_dummy]  else pp_es'
- 3808 |       | Tex _ -> pp_es'
- 3809 |       | Caml _ | Isa _ | Hol _ | Lem _ -> 
- 3810 |           ["[(" ^ String.concat "," pp_es ^ ")]",TTC_dummy]
- ...
- 3817 | 	    then [ "(cons " ^ List.hd pp_es ^ " nil)",TTC_dummy]
- 3818 | 	    else ["(cons " ^ "(" ^ String.concat "," pp_es ^ ") nil)",TTC_dummy]
- 3819 |       | Twf _ -> raise TwelfNotImplemented
- 3820 |       | Lex _ | Menhir _ -> raise ThisCannotHappen)
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "grammar_pp.ml", lines 4110-4113, characters 16-45:
- 4110 | ................(match hse with 
- 4111 |     | Hom_string _ -> arity_of_homspec hs'
- 4112 |     | Hom_index i -> max (1+i) (arity_of_homspec hs')
- 4113 |     | Hom_terminal _ -> arity_of_homspec hs')
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Hom_ln_free_index (_, _)
- File "grammar_pp.ml", lines 4356-4366, characters 19-24:
- 4356 | ...................match m with 
- 4357 |   | Coq _ -> "Coq"
- 4358 |   | Isa _ -> "Isa"
- 4359 |   | Hol _ -> "Hol"
- 4360 |   | Lem _ -> "Lem"
- ...
- 4363 |   | Tex _ -> "Tex"
- 4364 |   | Caml _ -> "Caml"
- 4365 |   | Lex _  -> "Lex"
- 4366 |   | Menhir _ -> "Menhir"
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -c -I ../ocamlgraph-1.7 parse_table.ml
- File "parse_table.ml", line 914, characters 42-56:
- 914 |                             prod_action = (fun [r] -> r);
-                                                 ^^^^^^^^^^^^^^
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (_::_::_|[])
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -c -I ../ocamlgraph-1.7 glr.ml
- File "glr.ml", line 455, characters 24-42:
- 455 |       let compare x y = Pervasives.compare x.sn_index y.sn_index
-                               ^^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -c -I ../ocamlgraph-1.7 new_term_parser.ml
- File "new_term_parser.ml", lines 150-177, characters 10-30:
- 150 | ..........(function 
- 151 |              | "[" -> "lbrac"
- 152 |              | "]" -> "rbrac"
- 153 |              | "!" -> "excl"
- 154 |              | "\"" -> "doublequote"
- ...
- 174 |              | "}" -> "rcurly"
- 175 |              | "|" -> "bar"
- 176 |              | "~" -> "tilde"
- 177 |              | "-" -> "minus")
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- ""
- File "new_term_parser.ml", lines 289-290, characters 14-18:
- 289 | ..............[Res_char c; Res_charl l] =
- 290 |   Res_charl (c::l)..
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Res_char _::Res_charl _::_::_|
- Res_char _::
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
- Res_string _|Res_int _|Res_si _|Res_sil _)::_|Res_char _::[]|
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_charl _|
- Res_string _|Res_int _|Res_si _|Res_sil _)::_|[])
- File "new_term_parser.ml", lines 292-293, characters 20-46:
- 292 | ....................[Res_char c; Res_charl l] =
- 293 |   Res_string (Auxl.string_of_char_list (c::l))..
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Res_char _::Res_charl _::_::_|
- Res_char _::
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
- Res_string _|Res_int _|Res_si _|Res_sil _)::_|Res_char _::[]|
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_charl _|
- Res_string _|Res_int _|Res_si _|Res_sil _)::_|[])
- File "new_term_parser.ml", line 295, characters 14-58:
- 295 | let res_stlil [Res_stli a; Res_stlil b] = Res_stlil (a::b);;
-                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Res_stli _::Res_stlil _::_::_|
- Res_stli _::
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_char _|Res_charl _|
- Res_string _|Res_int _|Res_si _|Res_sil _)::_|Res_stli _::[]|
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stlil _|Res_char _|Res_charl _|
- Res_string _|Res_int _|Res_si _|Res_sil _)::_|[])
- File "new_term_parser.ml", lines 342-346, characters 67-66:
- 342 | ...................................................................function
- 343 |       [] -> []
- 344 |     | Res_ignore::rl -> process_prod_res rl
- 345 |     | Res_ste ste::rl -> ste::process_prod_res rl
- 346 |     | Res_st st::rl -> Ste_st (dummy_loc, st)::process_prod_res rl
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Res_none|Res_stli _|Res_stlil _|Res_char _|Res_charl _|Res_string _|
- Res_int _|Res_si _|Res_sil _)::_
- File "new_term_parser.ml", line 382, characters 14-42:
- 382 |               (fun [Res_stlil x] -> elc x);
-                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Res_stlil _::_::_|
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_char _|Res_charl _|
- Res_string _|Res_int _|Res_si _|Res_sil _)::_|[])
- File "new_term_parser.ml", line 401, characters 8-42:
- 401 |         (fun [Res_stli x]-> Res_stlil [x]);
-               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Res_stli _::_::_|
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stlil _|Res_char _|Res_charl _|
- Res_string _|Res_int _|Res_si _|Res_sil _)::_|[])
- File "new_term_parser.ml", line 416, characters 16-51:
- 416 |                 (fun [x; _; y] -> res_stlil [x; y])
-                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (_::_::_::_::_|_::_::[]|_::[]|[])
- File "new_term_parser.ml", lines 463-467, characters 26-65:
- 463 | ..........................(fun [Res_stli (Stli_single (_, es1)); 
- 464 |                                 _; 
- 465 |                                 Res_int n';
- 466 |                                 Res_stli (Stli_single (_, es2))] ->
- 467 |                              process_dot_listform_res es1 n' es2).
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Res_stli (Stli_single (_, _))::_::Res_int _::Res_stli (Stli_single (_, _))::
-  _::_|
- Res_stli (Stli_single (_, _))::_::Res_int _::
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stlil _|Res_char _|Res_charl _|
- Res_string _|Res_int _|Res_si _|Res_sil _)::_|
- Res_stli (Stli_single (_, _))::_::Res_int _::[]|
- Res_stli (Stli_single (_, _))::_::
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
- Res_charl _|Res_string _|Res_si _|Res_sil _)::_|
- Res_stli (Stli_single (_, _))::_::[]|Res_stli (Stli_single (_, _))::[]|
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stlil _|Res_char _|Res_charl _|
- Res_string _|Res_int _|Res_si _|Res_sil _)::_|[])
- File "new_term_parser.ml", lines 476-482, characters 26-65:
- 476 | ..........................(fun [Res_stli (Stli_single (_, es1)); 
- 477 |                                 _; 
- 478 |                                 _;
- 479 |                                 Res_int n';
- 480 |                                 _;
- 481 |                                 Res_stli (Stli_single (_, es2))] ->
- 482 |                              process_dot_listform_res es1 n' es2)
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Res_stli (Stli_single (_, _))::_::_::Res_int _::_::
-  Res_stli (Stli_single (_, _))::_::_|
- Res_stli (Stli_single (_, _))::_::_::Res_int _::_::
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stlil _|Res_char _|Res_charl _|
- Res_string _|Res_int _|Res_si _|Res_sil _)::_|
- Res_stli (Stli_single (_, _))::_::_::Res_int _::_::[]|
- Res_stli (Stli_single (_, _))::_::_::Res_int _::[]|
- Res_stli (Stli_single (_, _))::_::_::
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
- Res_charl _|Res_string _|Res_si _|Res_sil _)::_|
- Res_stli (Stli_single (_, _))::_::_::[]|Res_stli (Stli_single (_, _))::_::[]|
- Res_stli (Stli_single (_, _))::[]|
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stlil _|Res_char _|Res_charl _|
- Res_string _|Res_int _|Res_si _|Res_sil _)::_|[])
- File "new_term_parser.ml", lines 488-500, characters 18-53:
- 488 | ..................(fun [_; Res_stli (Stli_single (_, es)); _; _; Res_string ivr;
- 489 |                         _] ->
- 490 |                      let es'' = 
- 491 |                        List.map 
- 492 |                          (Merge.abstract_indexvar_symterm_element ivr 0) 
- ...
- 497 |                                  stl_elements = es'';
- 498 |                                  stl_loc = dummy_loc}
- 499 |                      in
- 500 |                        Res_stli (Stli_listform stlb)).
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (_::Res_stli (Stli_single (_, _))::_::_::Res_string _::_::_::_|
- _::Res_stli (Stli_single (_, _))::_::_::Res_string _::[]|
- _::Res_stli (Stli_single (_, _))::_::_::
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
- Res_charl _|Res_int _|Res_si _|Res_sil _)::_|
- _::Res_stli (Stli_single (_, _))::_::_::[]|
- _::Res_stli (Stli_single (_, _))::_::[]|_::Res_stli (Stli_single (_, _))::[]|
- _::
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stlil _|Res_char _|Res_charl _|
- Res_string _|Res_int _|Res_si _|Res_sil _)::_|_::[]|[])
- File "new_term_parser.ml", lines 508-523, characters 18-53:
- 508 | ..................(fun [_; Res_stli (Stli_single (_, es)); _; _; Res_string ivr;
- 509 |                         _;
- 510 |                         _; Res_string ivr';
- 511 |                         _] ->
- 512 |                      let es'' = 
- ...
- 520 |                      let stlb = {stl_bound = b;
- 521 |                                  stl_elements = es'';
- 522 |                                  stl_loc = dummy_loc} in
- 523 |                        Res_stli (Stli_listform stlb)).
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (_::Res_stli (Stli_single (_, _))::_::_::Res_string _::_::_::Res_string _::
-  _::_::_|
- _::Res_stli (Stli_single (_, _))::_::_::Res_string _::_::_::Res_string _::[]|
- _::Res_stli (Stli_single (_, _))::_::_::Res_string _::_::_::
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
- Res_charl _|Res_int _|Res_si _|Res_sil _)::_|
- _::Res_stli (Stli_single (_, _))::_::_::Res_string _::_::_::[]|
- _::Res_stli (Stli_single (_, _))::_::_::Res_string _::_::[]|
- _::Res_stli (Stli_single (_, _))::_::_::Res_string _::[]|
- _::Res_stli (Stli_single (_, _))::_::_::
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
- Res_charl _|Res_int _|Res_si _|Res_sil _)::_|
- _::Res_stli (Stli_single (_, _))::_::_::[]|
- _::Res_stli (Stli_single (_, _))::_::[]|_::Res_stli (Stli_single (_, _))::[]|
- _::
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stlil _|Res_char _|Res_charl _|
- Res_string _|Res_int _|Res_si _|Res_sil _)::_|_::[]|[])
- File "new_term_parser.ml", lines 536-557, characters 18-53:
- 536 | ..................(fun [_; Res_stli (Stli_single (_, es)); _; _; Res_string ivr;
- 537 |                         _;
- 538 |                         _;
- 539 |                         Res_string lower;
- 540 |                         _;
- ...
- 554 |                      let stlb = {stl_bound = b;
- 555 |                                  stl_elements = es'';
- 556 |                                  stl_loc = dummy_loc} in
- 557 |                        Res_stli (Stli_listform stlb)).
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (_::Res_stli (Stli_single (_, _))::_::_::Res_string _::_::_::Res_string _::
-  _::Res_int _::_::Res_si _::_::_::_|
- _::Res_stli (Stli_single (_, _))::_::_::Res_string _::_::_::Res_string _::_::
- Res_int _::_::Res_si _::[]|
- _::Res_stli (Stli_single (_, _))::_::_::Res_string _::_::_::Res_string _::_::
- Res_int _::_::
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
- Res_charl _|Res_string _|Res_int _|Res_sil _)::_|
- _::Res_stli (Stli_single (_, _))::_::_::Res_string _::_::_::Res_string _::_::
- Res_int _::_::[]|
- _::Res_stli (Stli_single (_, _))::_::_::Res_string _::_::_::Res_string _::_::
- Res_int _::[]|
- _::Res_stli (Stli_single (_, _))::_::_::Res_string _::_::_::Res_string _::_::
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
- Res_charl _|Res_string _|Res_si _|Res_sil _)::_|
- _::Res_stli (Stli_single (_, _))::_::_::Res_string _::_::_::Res_string _::_::
- []|
- _::Res_stli (Stli_single (_, _))::_::_::Res_string _::_::_::Res_string _::[]|
- _::Res_stli (Stli_single (_, _))::_::_::Res_string _::_::_::
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
- Res_charl _|Res_int _|Res_si _|Res_sil _)::_|
- _::Res_stli (Stli_single (_, _))::_::_::Res_string _::_::_::[]|
- _::Res_stli (Stli_single (_, _))::_::_::Res_string _::_::[]|
- _::Res_stli (Stli_single (_, _))::_::_::Res_string _::[]|
- _::Res_stli (Stli_single (_, _))::_::_::
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
- Res_charl _|Res_int _|Res_si _|Res_sil _)::_|
- _::Res_stli (Stli_single (_, _))::_::_::[]|
- _::Res_stli (Stli_single (_, _))::_::[]|_::Res_stli (Stli_single (_, _))::[]|
- _::
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stlil _|Res_char _|Res_charl _|
- Res_string _|Res_int _|Res_si _|Res_sil _)::_|_::[]|[])
- File "new_term_parser.ml", line 560, characters 18-53:
- 560 |                   (fun [Res_stli x] -> Res_stlil [x]));
-                         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Res_stli _::_::_|
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stlil _|Res_char _|Res_charl _|
- Res_string _|Res_int _|Res_si _|Res_sil _)::_|[])
- File "new_term_parser.ml", line 574, characters 24-59:
- 574 |                         (fun [x; _; y] -> res_stlil [x; y]));
-                               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (_::_::_::_::_|_::_::[]|_::[]|[])
- File "new_term_parser.ml", line 603, characters 15-44:
- 603 |                (fun (_::rl) -> build_res rl) in
-                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- []
- File "new_term_parser.ml", line 609, characters 15-44:
- 609 |                (fun (_::rl) -> build_res rl) in
-                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- []
- File "new_term_parser.ml", line 628, characters 12-29:
- 628 |             (fun [_; x] -> x)
-                   ^^^^^^^^^^^^^^^^^
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (_::_::_::_|_::[]|[])
- File "new_term_parser.ml", lines 638-639, characters 13-63:
- 638 | .............(fun [_; Res_sil l] ->
- 639 |                 Res_st (St_nonterm (dummy_loc, ntr, (nt', l)))).
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (_::Res_sil _::_::_|
- _::
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
- Res_charl _|Res_string _|Res_int _|Res_si _)::_|_::[]|[])
- File "new_term_parser.ml", lines 649-653, characters 18-55:
- 649 | ..................(fun [_; Res_sil l] ->
- 650 |                      Res_st (St_nontermsub (dummy_loc, 
- 651 |                                             ntl, 
- 652 |                                             Auxl.promote_ntr xd ntr, 
- 653 |                                             (nt', l)))).
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (_::Res_sil _::_::_|
- _::
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
- Res_charl _|Res_string _|Res_int _|Res_si _)::_|_::[]|[])
- File "new_term_parser.ml", lines 664-665, characters 6-59:
- 664 | ......(fun [_; Res_sil x] ->
- 665 |          Res_ste (Ste_metavar (dummy_loc, name, (mvr, x))))
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (_::Res_sil _::_::_|
- _::
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
- Res_charl _|Res_string _|Res_int _|Res_si _)::_|_::[]|[])
- File "new_term_parser.ml", line 695, characters 14-100:
- 695 |               (fun (_::Res_string s::_) -> Res_ste (Ste_metavar (dummy_loc, mvd.mvd_name, (s, []))))
-                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (_::
-  (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
-  Res_charl _|Res_int _|Res_si _|Res_sil _)::_|
- _::[]|[])
- File "new_term_parser.ml", lines 703-707, characters 16-68:
- 703 | ................(fun [_; Res_string s] -> 
- 704 |                    if is_tm s then
- 705 |                      raise Reject_parse
- 706 |                    else
- 707 |                      Res_ste (Ste_var (dummy_loc, mvd.mvd_name, s))).
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (_::Res_string _::_::_|
- _::
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
- Res_charl _|Res_int _|Res_si _|Res_sil _)::_|_::[]|[])
- File "new_term_parser.ml", lines 710-711, characters 16-66:
- 710 | ................(fun [_; Res_string s] -> 
- 711 |                    Res_ste (Ste_var (dummy_loc, mvd.mvd_name, s))).
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (_::Res_string _::_::_|
- _::
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
- Res_charl _|Res_int _|Res_si _|Res_sil _)::_|_::[]|[])
- File "new_term_parser.ml", lines 715-719, characters 16-23:
- 715 | ................(fun [((Res_ste (Ste_var (_, _, s))) as x)] -> 
- 716 |                    if is_tm s then 
- 717 |                      raise Reject_parse
- 718 |                    else
- 719 |                      x)
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Res_ste (Ste_var (_, _, _))::_::_|
- Res_ste (Ste_st (_, _)|Ste_list (_, _))::_|
- (Res_ignore|Res_none|Res_st _|Res_stli _|Res_stlil _|Res_char _|Res_charl _|
- Res_string _|Res_int _|Res_si _|Res_sil _)::_|[])
- File "new_term_parser.ml", line 742, characters 6-41:
- 742 |       (fun [Res_char c] -> Res_charl [c]);
-             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Res_char _::_::_|
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_charl _|
- Res_string _|Res_int _|Res_si _|Res_sil _)::_|[])
- File "new_term_parser.ml", line 748, characters 6-68:
- 748 |       (fun [Res_charl s] -> Res_string (Auxl.string_of_char_list s));
-             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Res_charl _::_::_|
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
- Res_string _|Res_int _|Res_si _|Res_sil _)::_|[])
- File "new_term_parser.ml", line 761, characters 6-53:
- 761 |       (fun [Res_si s; Res_sil sl] -> Res_sil (s::sl));
-             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Res_si _::Res_sil _::_::_|
- Res_si _::
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
- Res_charl _|Res_string _|Res_int _|Res_si _)::_|Res_si _::[]|
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
- Res_charl _|Res_string _|Res_int _|Res_sil _)::_|[])
- File "new_term_parser.ml", line 767, characters 6-73:
- 767 |       (fun [Res_charl l] -> Res_si (Si_num (Auxl.string_of_char_list l)));
-             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Res_charl _::_::_|
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
- Res_string _|Res_int _|Res_si _|Res_sil _)::_|[])
- File "new_term_parser.ml", line 771, characters 6-24:
- 771 |       (fun [rsi] -> rsi);
-             ^^^^^^^^^^^^^^^^^^
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (_::_::_|[])
- File "new_term_parser.ml", line 794, characters 6-47:
- 794 |       (fun [Res_charl c] -> Res_charl ('_'::c));
-             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Res_charl _::_::_|
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
- Res_string _|Res_int _|Res_si _|Res_sil _)::_|[])
- File "new_term_parser.ml", line 796, characters 6-48:
- 796 |       (fun [Res_charl c] -> Res_charl ('\''::c));
-             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Res_charl _::_::_|
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
- Res_string _|Res_int _|Res_si _|Res_sil _)::_|[])
- File "new_term_parser.ml", line 831, characters 6-52:
- 831 |       (fun [Res_string s] -> Res_si (Si_var (s, 0)));
-             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Res_string _::_::_|
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
- Res_charl _|Res_int _|Res_si _|Res_sil _)::_|[])
- File "new_term_parser.ml", line 835, characters 6-53:
- 835 |       (fun [Res_string s] -> Res_si (Si_var (s, -1)));
-             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Res_string _::_::_|
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
- Res_charl _|Res_int _|Res_si _|Res_sil _)::_|[])
- File "new_term_parser.ml", lines 846-847, characters 13-61:
- 846 | .............(fun [_; Res_sil x] ->
- 847 |                 Res_st (St_nonterm (dummy_loc, "", (nt, x)))).
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (_::Res_sil _::_::_|
- _::
- (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _|
- Res_charl _|Res_string _|Res_int _|Res_si _)::_|_::[]|[])
- File "new_term_parser.ml", line 858, characters 13-27:
- 858 |              (fun [x] -> x);
-                    ^^^^^^^^^^^^^^
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (_::_::_|[])
- ocamlc -g -dtypes   -I ../ocamlgraph-1.7 -c term_parser.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I ../ocamlgraph-1.7 -c term_parser.ml
- File "term_parser.ml", line 1214, characters 25-54:
- 1214 |                 List.map (fun (Ntp.Gtp.Res_st s) -> s) res
-                                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Res_ignore|Res_none|Res_ste _|Res_stli _|Res_stlil _|Res_char _|Res_charl _|
- Res_string _|Res_int _|Res_si _|Res_sil _)
- ocamlc -g -dtypes   -I ../ocamlgraph-1.7 -c dependency.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -c -I ../ocamlgraph-1.7 dependency.ml
- File "dependency.ml", lines 571-579, characters 2-69:
- 571 | ..match m with
- 572 |   | Isa io when io.ppi_isa_primrec -> isa_primrec_collapse m xd funcs
- 573 |   | Isa io when not io.ppi_isa_primrec -> isa_fun_collapse m xd funcs
- 574 |   | Hol _ -> hol_collapse m xd funcs
- 575 |   | Lem _ -> lem_collapse m xd funcs
- 576 |   | Coq _ -> coq_collapse m xd funcs
- 577 |   | Twf _ -> twf_collapse m xd funcs
- 578 |   | Caml _ -> caml_collapse m xd funcs
- 579 |   | Tex _ | Ascii _ -> Auxl.error "internal: collapse of Tex-Ascii\n"
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Isa _|Rdx _|Lex _|Menhir _)
- (However, some guarded clause may match this value.)
- File "dependency.ml", lines 584-714, characters 2-53:
- 584 | ..match m with
- 585 |   | Tex _ | Ascii _ -> Auxl.error "internal: print of Tex-Ascii\n"
- 586 |   | Isa io ->
- 587 |       let print_lemma block = 
- 588 | 	if ( List.exists 
- ...
- 711 | (*               (List.map (fun (_,((h1,h2,h3),s,_)) -> h1 ^ "FOO1" ^ h2 ^ "FOO2"^ h3 ^ "FOO3"^s) block))*)
- 712 |                (List.map (fun (_,((h1,h2,h3),s,_)) -> h1 ^ h2 ^ h3 ^ s ^ "  end\n") block))
- 713 | 	  ^ "\n") in
- 714 |       String.concat "" (List.map print_block sorting)
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Rdx _|Lex _|Menhir _)
- ocamlc -g -dtypes   -I ../ocamlgraph-1.7 -c bounds.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I ../ocamlgraph-1.7 -c bounds.ml
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I ../ocamlgraph-1.7 -c context_pp.ml
- File "context_pp.ml", lines 103-106, characters 4-57:
- 103 | ....( match m with
- 104 |     | Coq _ | Caml _ -> lhs_pat 
- 105 |     | Isa _ | Hol _ | Lem _ | Twf _ -> lhs_pat ^ " " ^ Grammar_pp.pp_nonterm m xd hole
- 106 |     | Lex _ | Menhir _ | Tex _ | Ascii _ -> assert false)...
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "context_pp.ml", lines 126-148, characters 4-5:
- 126 | ....( match m with
- 127 |     | Coq _ ->
- 128 | 	( id 
- 129 | 	  ^ " ("^ctx_var^":"^ Grammar_pp.pp_nontermroot_ty m xd cr.cr_ntr 
- 130 | 	  ^ ") ("^fake_hole_var^":"^ Grammar_pp.pp_nontermroot_ty m xd cr.cr_hole ^")",
- ...
- 145 | 	  " : " ^ (Grammar_pp.pp_nontermroot_ty m xd cr.cr_target) ^ " =\n  match "^ctx_var^" with\n")
- 146 |     | Twf _ -> Auxl.errorm m "pp_rule_context"
- 147 |     | Lex _ | Menhir _ | Tex _ | Ascii _ -> assert false
- 148 |     )...
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I ../ocamlgraph-1.7 -c quotient_rules.ml
- ocamlc -g -dtypes   -I ../ocamlgraph-1.7 -c grammar_typecheck.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -c -I ../ocamlgraph-1.7 grammar_typecheck.ml
- File "grammar_typecheck.ml", line 121, characters 86-103:
- 121 |     { raw_prod_name = (if rr.raw_rule_pn_wrapper<>"" then rr.raw_rule_pn_wrapper else String.capitalize rr.raw_rule_ntr_name ^"_") ^ "aux";
-                                                                                             ^^^^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.String.capitalize
- Use String.capitalize_ascii instead.
- ocamlc -g -dtypes   -I ../ocamlgraph-1.7 -c transform.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I ../ocamlgraph-1.7 -c transform.ml
- ocamlc -g -dtypes   -I ../ocamlgraph-1.7 -c substs_pp.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I ../ocamlgraph-1.7 -c substs_pp.ml
- File "substs_pp.ml", lines 147-150, characters 20-34:
- 147 | ....................match m with 
- 148 |   | Coq co -> Auxl.add_to_lib co.coq_library "list_mem" pp_list_mem_coq
- 149 |   | Caml _ | Hol _ | Lem _ | Isa _ | Tex _ | Twf _ | Ascii _ | Lex _ | Menhir _ 
- 150 |     -> Auxl.errorm m "pp_list_mem"
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "substs_pp.ml", lines 152-155, characters 23-37:
- 152 | .......................match m with
- 153 |   | Coq co -> Auxl.add_to_lib co.coq_library "list_filter" pp_list_filter_coq
- 154 |   | Isa _ | Hol _ | Lem _ | Caml _ | Tex _ | Twf _ | Ascii _ | Lex _ | Menhir _ 
- 155 |     -> Auxl.errorm m "pp_list_filter"
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "substs_pp.ml", lines 157-165, characters 22-79:
- 157 | ......................match m with 
- 158 |   | Caml oo -> Auxl.add_to_lib oo.caml_library "list_minus" pp_list_minus_caml
- 159 |   | Lem oo -> Auxl.add_to_lib oo.lem_library "list_minus" pp_list_minus_lem
- 160 |   | Isa io  -> Auxl.add_to_lib io.isa_library "list_minus" pp_list_minus_isa
- 161 |   | Hol ho  -> ()
- 162 |   | Coq co  ->
- 163 |       pp_list_mem m;
- 164 |       Auxl.add_to_lib co.coq_library "list_minus" pp_list_minus_coq
- 165 |   | Tex _ | Twf _ | Ascii _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_list_minus"
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "substs_pp.ml", lines 167-172, characters 23-37:
- 167 | .......................match m with 
- 168 |   | Coq co ->
- 169 |       pp_list_mem m;
- 170 |       Auxl.add_to_lib co.coq_library "list_minus2" pp_list_minus2_coq
- 171 |   | Caml _ | Hol _ | Lem _ | Isa _ | Twf _ | Tex _ | Ascii _ | Lex _ | Menhir _ 
- 172 |     -> Auxl.errorm m "pp_list_minus2"
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "substs_pp.ml", lines 174-180, characters 22-36:
- 174 | ......................match m with 
- 175 |   | Isa io -> Auxl.add_to_lib io.isa_library "list_assoc" pp_list_assoc_isa
- 176 |   | Hol ho -> ()
- 177 |   | Lem lo -> Auxl.add_to_lib lo.lem_library "list_assoc" pp_list_assoc_lem
- 178 |   | Coq co -> Auxl.add_to_lib co.coq_library "list_assoc" pp_list_assoc_coq
- 179 |   | Caml _ | Twf _ | Tex _ | Ascii _ | Lex _ | Menhir _ 
- 180 |     -> Auxl.errorm m "pp_list_assoc"
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "substs_pp.ml", lines 333-336, characters 10-11:
- 333 | ..........(match m with 
- 334 |           | Caml _ -> Grammar_pp.pp_nt_or_mv_root_ty m xd ntmvr ^ " list" 
- 335 |           | Lem _ -> "list " ^Grammar_pp.pp_nt_or_mv_root_ty m xd ntmvr
- 336 |           )
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Coq _|Isa _|Hol _|Twf _|Rdx _|Ascii _|Tex _|Lex _|Menhir _)
- File "substs_pp.ml", lines 306-339, characters 4-86:
- 306 | ....( match m with
- 307 |     | Isa _ -> 
- 308 | 	( Auxl.auxfn_name f ntrn ntrn (* FZ *)
- 309 | 	  ^ " :: \""
- 310 | 	  ^ Grammar_pp.pp_nontermroot_ty m xd ntr ^" => "
- ...
- 336 |           )
- 337 |           ^" =\n" 
- 338 | 	  ^ "  match " ^ Grammar_pp.pp_nonterm m xd pat_var ^ " with\n" ) 
- 339 |     | Twf _ | Tex _ | Ascii _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_auxfn_clauses" ).
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "substs_pp.ml", lines 576-605, characters 10-82:
- 576 | ..........match m with
- 577 |           | Isa _ ->
- 578 |               that_s 
- 579 |               ^" : set "
- 580 |               ^ Grammar_pp.pp_mse_string m xd sie de bound_things_glommed
- ...
- 602 | 	      ^ that_s ^ " "
- 603 | 	      ^ ( match Grammar_pp.pp_mse m xd sie de false "" (Some subst.sb_that) bound_things_glommed with x,_,_ -> x)
- 604 | 	  | Twf _ -> "<<< mem FZ no idea >>>"
- 605 |           | Tex _ | Ascii _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_subst_symterm"
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "substs_pp.ml", lines 612-698, characters 12-84:
- 612 | ............match m with
- 613 |             | Isa _ -> 
- 614 | 		"("
- 615 | 		^ Auxl.subst_name subst.sb_name dep_name ^ " "
- 616 | 		^ (match bound_things_glommed with
- ...
- 695 | 		^ nt_s
- 696 | 		^ ")"
- 697 | 	    | Twf _ -> "<<< filter FZ no idea >>>"
- 698 |             | Tex _ | Ascii _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_subst_symterm"..
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "substs_pp.ml", lines 811-933, characters 4-86:
- 811 | ....match m with
- 812 |     | Isa _ | Hol _ | Lem _ ->
- 813 |         let typ = (Grammar_pp.make_name_elements m xd true stlb.stl_elements) ^ " list" in
- 814 | 	let split_suffix = 
- 815 | 	  ( match m with
- ...
- 930 | 
- 931 |     | Caml _ -> ("",[])
- 932 | 
- 933 |     | Twf _ | Tex _ | Ascii _ | Lex _ | Menhir _ -> Auxl.errorm m "make_aux_func_list"
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "substs_pp.ml", lines 1030-1063, characters 4-82:
- 1030 | ....match m with
- 1031 |     | Isa _ ->   
- 1032 | (*           "(List.map (%"^pp_pattern^"."^pp_body^") "  *)
- 1033 | (*           ^ pp_squished_vars *)
- 1034 | (*           ^ ")", [] *)
- ...
- 1060 |         ( lemTODO "20" " (List.map (fun "^de1i.de1_pattern^" -> "^pp_body^") "
- 1061 |         ^ de1i.de1_compound_id
- 1062 |         ^ ")", [] )
- 1063 |     | Twf _ | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.errorm m "make_aux_funcs"
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "substs_pp.ml", lines 1088-1095, characters 6-76:
- 1088 | ......( match m with 
- 1089 |       | Coq _ | Caml _ | Lem _ -> lhs_pat  
- 1090 |       | Isa _ | Hol _ | Twf _ -> 
- 1091 | (*           Auxl.subst_name subst.sb_name rule_ntr_name  ^ " " *)
- 1092 |           ( if subst.sb_multiple then sub_var
- 1093 |           else Grammar_pp.pp_nonterm m xd this_var ^ " " ^ Grammar_pp.pp_nt_or_mv m xd that_var )
- 1094 |           ^ " " ^ lhs_pat 
- 1095 |       | Tex _ | Ascii _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_subst_prod")...
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "substs_pp.ml", lines 1118-1173, characters 14-84:
- 1118 | ..............(match m with
- 1119 |               | Isa _ -> 
- 1120 | 		  pp_list_assoc m;
- 1121 | 		  (* tentative isa code for multiple subst *)
- 1122 | 		  "(case list_assoc " 
- ...
- 1170 | 		  ^ sub_var 
- 1171 | 		  ^ " with Not_found -> " ^ lhs_pat 
- 1172 | 		  ^ ")" 
- 1173 | 	      | Twf _ | Tex _ | Ascii _ | Lex _ | Menhir _ -> raise Auxl.ThisCannotHappen )
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "substs_pp.ml", lines 1178-1188, characters 2-71:
- 1178 | ..( match m with
- 1179 | 		| Isa _ | Hol _ | Lem _ | Caml _ -> thing_s ^ "=" ^ that_s
- 1180 | 		| Twf _ -> raise Auxl.ThisCannotHappen
- 1181 | 		| Coq _ ->
- 1182 | 		    ( if Auxl.require_locally_nameless xd 
- ...
- 1185 | 		    ^ " "
- 1186 | 		    ^ thing_s ^ " " 
- 1187 | 		    ^ that_s
- 1188 | 		| Tex _ | Ascii _ | Lex _ | Menhir _ -> raise Auxl.ThisCannotHappen )...
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "substs_pp.ml", lines 1114-1204, characters 6-8:
- 1114 | ......( match m with
- 1115 |       | Coq _ | Isa _ | Hol _ | Lem _ | Caml _ ->
- 1116 | 	  let ssr = 
- 1117 | 	    if subst.sb_multiple then 
- 1118 |               (match m with
- ...
- 1201 | 
- 1202 |       | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_subst_prod"
- 1203 | 
- 1204 |        )
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "substs_pp.ml", line 1240, characters 16-33:
- 1240 |                 String.capitalize lhs_stnb.st_prod_name  
-                        ^^^^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.String.capitalize
- Use String.capitalize_ascii instead.
- File "substs_pp.ml", line 1248, characters 16-33:
- 1248 |                 String.capitalize lhs_stnb.st_prod_name  
-                        ^^^^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.String.capitalize
- Use String.capitalize_ascii instead.
- File "substs_pp.ml", lines 1400-1412, characters 3-4:
- 1400 | ...(match m with 
- 1401 | 		 | Caml _ -> 	
- 1402 | 		     "(" 
- 1403 | 	             ^ Grammar_pp.pp_nt_or_mv_root_ty m xd subst.sb_that 
- 1404 | 		     ^ "*" ^ Grammar_pp.pp_nontermroot_ty m xd subst.sb_this 
- ...
- 1409 | 		     ^ Grammar_pp.pp_nt_or_mv_root_ty m xd subst.sb_that 
- 1410 | 		     ^ "*" ^ Grammar_pp.pp_nontermroot_ty m xd subst.sb_this 
- 1411 | 		     ^ ")"
- 1412 | 		 )
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Coq _|Isa _|Hol _|Twf _|Rdx _|Ascii _|Tex _|Lex _|Menhir _)
- File "substs_pp.ml", lines 1374-1438, characters 6-73:
- 1374 | ......( match m with 
- 1375 |       | Coq _ ->       
- 1376 | 	  ( (id
- 1377 |              ^ ( if subst.sb_multiple 
- 1378 | 	     then 
- ...
- 1435 |                ^ Grammar_pp.pp_nontermroot_ty m xd r.rule_ntr_name ^ " -> "
- 1436 | 	       ^ Grammar_pp.pp_nontermroot_ty m xd r.rule_ntr_name ^ " -> type.\n")
- 1437 | 	    )  , "", "")
- 1438 |       | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.error "pp_subst_rule")
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "substs_pp.ml", lines 1542-1545, characters 5-65:
- 1542 | .....( match m with 
- 1543 | 	    | Twf _ -> Some call
- 1544 | 	    | Isa _ | Hol _ | Lem _ | Caml _ | Coq _ -> Some ("("^call^")")
- 1545 |             | Tex _ | Ascii _ | Lex _ | Menhir _ -> assert false).
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "substs_pp.ml", lines 1582-1585, characters 2-77:
- 1582 | ..(match m with (* HACK is the name eq_thing always correct? *) 
- 1583 | 		| Ascii _ | Tex _ | Twf _ | Lex _ | Menhir _ -> Auxl.errorm m "list_minus"
- 1584 | 		| Isa _ | Hol _ | Lem _ | Caml _ -> "" 
- 1585 | 		| Coq _ -> "eq_" ^ (Grammar_pp.pp_nt_or_mv_root_ty m xd fv.fv_that) ^ " " ).
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "substs_pp.ml", lines 1565-1587, characters 15-82:
- 1565 | ...............( 
- 1566 | 	  ( match m with
- 1567 | 	  | Twf _ -> 
- 1568 | 	      let result = Auxl.fresh_nl () in
- 1569 | 	      let interm = Auxl.fresh_nl () in
- ...
- 1584 | 		| Isa _ | Hol _ | Lem _ | Caml _ -> "" 
- 1585 | 		| Coq _ -> "eq_" ^ (Grammar_pp.pp_nt_or_mv_root_ty m xd fv.fv_that) ^ " " ) 
- 1586 |               ^ s ^" "
- 1587 |               ^ Grammar_pp.pp_mse_string m xd sie de bound_things_glommed ^")")  )
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "substs_pp.ml", lines 1624-1629, characters 10-11:
- 1624 | ..........(match m with 
- 1625 |           | Isa _ | Hol _ | Lem _ | Caml _ -> ("["^mv_s^"]") 
- 1626 |           | Coq _ -> ("(cons "^mv_s^" nil)") 
- 1627 | 	  | Twf _ -> ("(natlist/cons "^mv_s^" natlist/nil)") 
- 1628 |           | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_fv_symterm_element"
- 1629 |           )....
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "substs_pp.ml", lines 1747-1876, characters 3-8:
- 1747 | ...( match m with 
- 1748 |           | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.error "pp_fv_symterm_list_body"
- 1749 | 	  | Isa io when io.ppi_isa_primrec ->
- 1750 |               let args = 
- 1751 | 	        String.concat "_" 
- ...
- 1873 | 		  ("(flat_map (fun (pat_:"^de1i.de1_coq_type_of_pattern^") => match pat_ with " ^ de1i.de1_pattern ^ " => "^pp_body^" end) "
- 1874 | 		   ^ de1i.de1_compound_id
- 1875 | 		   ^ ")"), funcs
- 1876 |        )..
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Coq _|Isa _|Twf _|Rdx _)
- (However, some guarded clause may match this value.)
- File "substs_pp.ml", lines 1718-1876, characters 2-10:
- 1718 | ..match m with
- 1719 |   | Twf _ | Tex _ | Ascii _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_fv_symterm_list_body"
- 1720 |   | Isa _ | Coq _ | Hol _ | Lem _ | Caml _ ->
- 1721 |       let pp_body_elements, funcs =
- 1722 | 	let body_options, funcs = 
- ...
- 1873 | 		  ("(flat_map (fun (pat_:"^de1i.de1_coq_type_of_pattern^") => match pat_ with " ^ de1i.de1_pattern ^ " => "^pp_body^" end) "
- 1874 | 		   ^ de1i.de1_compound_id
- 1875 | 		   ^ ")"), funcs
- 1876 |        ) )
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "substs_pp.ml", lines 1904-1913, characters 8-9:
- 1904 | ........(match m with 
- 1905 | 	| Isa _ when (List.exists (fun (x,_) -> x = "isa-set") fv.fv_homs) -> "{"^thing_s^"}"
- 1906 |         | Isa _ | Hol _ | Lem _ | Caml _ -> ("["^thing_s^"]") 
- 1907 |         | Coq co ->
- 1908 | 	    if not !(co.coq_locally_nameless)
- 1909 | 	    then "(cons "^thing_s^" nil)"
- 1910 | 	    else "{{"^thing_s^"}}"
- 1911 | 	| Twf _ -> ("(natlist/cons "^thing_s^" natlist/nil)") 
- 1912 |         | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.errorm m "freevar_singleton_rhs"
- 1913 |         )...
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "substs_pp.ml", lines 1951-1959, characters 7-86:
- 1951 | .......(match m with 
- 1952 | 	      | Isa _ when has_isa_set_hom fv -> "{}"
- 1953 | 	      | Isa _ | Hol _ | Lem _ | Caml _ -> "[]" 
- 1954 | 	      | Coq co -> 
- 1955 | 		  if not !(co.coq_locally_nameless)
- 1956 | 		  then "nil"
- 1957 | 		  else "{}"
- 1958 | 	      | Twf _ -> "natlist/nil"
- 1959 |               | Tex _ | Ascii _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_freevar_prod")
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "substs_pp.ml", lines 1961-1970, characters 7-86:
- 1961 | .......( match m with 
- 1962 | 	      | Isa _ when has_isa_set_hom fv -> String.concat " \\<union> " rhs_elements
- 1963 |               | Isa _ | Caml _ | Lem _ -> String.concat (list_append m) rhs_elements 
- 1964 |               | Hol _ -> String.concat " ++ " rhs_elements 
- 1965 | 	      | Coq co -> 
- 1966 | 		  if not !(co.coq_locally_nameless)
- 1967 | 		  then Auxl.insert_append m rhs_elements
- 1968 | 		  else String.concat " \\u " rhs_elements
- 1969 | 	      | Twf _ -> Auxl.insert_append m rhs_elements
- 1970 |               | Tex _ | Ascii _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_freevar_prod")
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "substs_pp.ml", lines 2030-2033, characters 5-6:
- 2030 | .....(match m with 
- 2031 | 	    | Caml _ -> Grammar_pp.pp_nt_or_mv_root_ty m xd fv.fv_that ^ " list"
- 2032 | 	    | Lem _ -> " list " ^ Grammar_pp.pp_nt_or_mv_root_ty m xd fv.fv_that
- 2033 | 	    )
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Coq _|Isa _|Hol _|Twf _|Rdx _|Ascii _|Tex _|Lex _|Menhir _)
- File "substs_pp.ml", lines 1997-2041, characters 6-78:
- 1997 | ......( match m with 
- 1998 |       | Coq co -> 
- 1999 | 	  let nts_used = Context_pp.nts_used_in_lhss m xd r in
- 2000 |           let fresh_var_ntr = Auxl.secondary_ntr xd r.rule_ntr_name  in
- 2001 | 	  let fresh_var = Auxl.fresh_nt nts_used (fresh_var_ntr,[]) in
- ...
- 2038 | 	    ^ Grammar_pp.pp_nontermroot_ty m xd r.rule_ntr_name ^ " -> "
- 2039 | 	    ^ "natlist -> type.\n" ), "", ""
- 2040 | 	  
- 2041 |       | Tex _ | Ascii _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_freevar_rule")
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- ocamlc -g -dtypes   -I ../ocamlgraph-1.7 -c subrules_pp.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I ../ocamlgraph-1.7 -c subrules_pp.ml
- File "subrules_pp.ml", lines 167-368, characters 8-2:
- 167 | ........( match m with 
- 168 |         | Isa io when io.ppi_isa_primrec ->
- 169 | 	    let typ = 
- 170 | 	      Auxl.the (Grammar_pp.pp_elements 
- 171 | 	       	 m xd  ((Si_punct "_")::sie) elbu.elb_es true false true true) ^ " list" in
- ...
- 365 |             [ " %{ TWELF NOT IMPLEMENTED }%"], deps, []
- 366 |         | Tex _ | Ascii _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_subelement"
- 367 | 
- 368 |  )
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Coq _|Isa _|Rdx _)
- (However, some guarded clause may match this value.)
- File "subrules_pp.ml", lines 426-432, characters 19-85:
- 426 | ...................match m with 
- 427 |                    | Coq _ | Hol _ | Lem _| Isa _ | Caml _ -> 
- 428 | 		       if conjuncts = [] 
- 429 |                        then Auxl.pp_true m false
- 430 | 		       else String.concat (Auxl.pp_and m false) conjuncts
- 431 |                    | Twf _ -> String.concat "" (List.map (function s -> " <- "^s) conjuncts)
- 432 |                    | Lex _ | Menhir _ | Tex _ | Ascii _ -> Auxl.errorm m "pp_subrule"
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "subrules_pp.ml", lines 436-449, characters 13-79:
- 436 | .............match m with 
- 437 |              | Coq _ | Hol _ | Lem _ | Isa _ | Caml _ -> 
- 438 |                  let rhs = 
- 439 |                    if rhss = [] 
- 440 |                    then Auxl.pp_false m false
- ...
- 446 |              | Twf _ -> 
- 447 | 		 let pfx = pu.prod_name in 
- 448 |                  List.map (fun rhs -> (pfx, lhs,rhs)) rhss
- 449 |              | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_subrule"
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "subrules_pp.ml", lines 457-492, characters 1-10:
- 457 | .( match m with 
- 458 | 	| Isa _ -> 
- 459 | 	    ( Auxl.pp_is srl sru ^ " :: \"" 
- 460 | 	      ^ Grammar_pp.pp_nontermroot_ty m xd sru
- 461 | 	      ^ " => bool\"\n", "","")
- ...
- 489 | 	      ^ Grammar_pp.pp_nontermroot_ty m xd sru
- 490 | 	      ^ " -> type.\n", "","")
- 491 |         | Tex _ | Ascii _ | Lex _ | Menhir _ -> Auxl.error "pp_subprod"
- 492 |          )...
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- ocamlc -g -dtypes   -I ../ocamlgraph-1.7 -c embed_pp.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I ../ocamlgraph-1.7 -c embed_pp.ml
- File "embed_pp.ml", lines 48-76, characters 2-123:
- 48 | ..match (m,hn) with 
- 49 |   | (Ascii ao, _) -> 
- 50 |       output_string fd Grammar_pp.pp_DOUBLELEFTBRACE;
- 51 |       output_string fd " ";
- 52 |       output_string fd (Grammar_pp.pp_hom_name m xd hn);
- ...
- 73 |   | (Isa io, "isa-lib") -> 
- 74 |       let x = io.isa_library in
- 75 |       x := (fst !x, embed_strings (snd !x) es)
- 76 |   | (Coq _, _) | (Isa _, _) | (Hol _,_) | (Lem _,_) | (Twf _,_) | (Tex _,_) | (Caml _,_) | (Lex _, _) | (Menhir _, _) -> ()
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Rdx _, "")
- ocamlc -g -dtypes   -I ../ocamlgraph-1.7 -c defns.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I ../ocamlgraph-1.7 -c defns.ml
- File "defns.ml", line 79, characters 30-46:
- 79 | 	    (( match m with Twf _ -> String.uppercase ntr' 
-                                    ^^^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.String.uppercase
- Use String.uppercase_ascii instead.
- File "defns.ml", lines 79-81, characters 6-83:
- 79 | ......( match m with Twf _ -> String.uppercase ntr' 
- 80 | 	    | Coq _ | Isa _ | Hol _ | Lem _ -> ntr'
- 81 | 	    | Caml _ | Tex _ | Ascii _ | Lex _ | Menhir _ -> raise Auxl.ThisCannotHappen )
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "defns.ml", lines 95-136, characters 17-17:
-  95 | .................match m with
-  96 |                  | Ascii _ | Tex _ | Caml _ | Twf _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_listsubntr"
-  97 |                  | Isa _ -> 
-  98 | (* Tobias says: should use  "ALL x : set xs. P x" rather than "list_all P xs", so...: *)
-  99 | (* TODO: choose a better internal name than x__ *)
- ...
- 133 | 		           then "(unmake_list_"^(String.concat "_" ty_list)^" "^ pp_squished_vars^")"
- 134 | 		           else pp_squished_vars )
- 135 | 		       ^ ")"
- 136 | 	             end.
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "defns.ml", lines 706-712, characters 2-34:
- 706 | ..match m with
- 707 |   | Ascii ao ->
- 708 |       ppd_lhs ^ " === " ^ ppd_rhs ^ "\n"
- 709 |   | Tex _ ->                                  
- 710 |       Grammar_pp.pp_tex_FUNCLAUSE_NAME m^"{"^ppd_lhs^"}"^"{"^ppd_rhs^"}%\n"
- 711 |   | Isa _ | Hol _ | Lem _ | Coq _ | Caml _ | Twf _ | Lex _ | Menhir _ -> 
- 712 |       Auxl.errorm m "pp_funclause"
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "defns.ml", lines 735-738, characters 1-76:
- 735 | .match m with
- 736 | 	| Coq _ | Caml _ | Lem _ (* LemTODO4: really? *) -> (insert_commas hom)
- 737 | 	| Hol _ | Isa _  -> hom
- 738 | 	| Twf _ | Ascii _ | Tex _ | Lex _ | Menhir _ -> raise Auxl.ThisCannotHappen
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "defns.ml", lines 745-842, characters 4-79:
- 745 | ....match m with
- 746 |     | Hol _ -> Some ("","","")
- 747 |     | Lem _ -> raise LemTODO (*LemTODO5*)
- 748 |     | Coq _ -> 
- 749 | 	let prod_name = fd.fd_pn_wrapper^ fd.fd_name in
- ...
- 839 | 	      (v,ms) 
- 840 | 	in
- 841 | 	Some ( fd.fd_name ^ " " ^ type_defn ^ ": " ^ result_type_name ^ "=\n", "", match_string)
- 842 |     | Tex _ | Ascii _ | Twf _ | Lex _ | Menhir _ -> raise Auxl.ThisCannotHappen.
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "defns.ml", lines 864-893, characters 2-32:
- 864 | ..match m with
- 865 |   | Ascii _ ->
- 866 |       Grammar_pp.pp_FUNDEFN ^"\n"
- 867 |       ^ Grammar_pp.pp_symterm m xd [] de_empty fd.fd_form
- 868 |       ^ Grammar_pp.pp_COLONCOLON ^" "^fd.fd_result^" "
- ...
- 890 |       ^ "}\n\n"
- 891 | 
- 892 |   | Isa _ | Hol _ | Lem _ | Coq _ | Twf _ | Caml _ | Lex _ | Menhir _ -> 
- 893 |       Auxl.errorm m "pp_fundefn"
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "defns.ml", lines 896-936, characters 2-26:
- 896 | ..match m with
- 897 |   | Ascii _ -> 
- 898 |       Grammar_pp.pp_FUNDEFNCLASS ^"\n"
- 899 |       ^ fdc.fdc_name ^" "
- 900 |       ^ Grammar_pp.pp_CCE^"\n\n"
- ...
- 933 | 	(Dependency.compute m xd int_funcs_collapsed)
- 934 | 
- 935 |   | Twf _ -> Auxl.warning "internal: fundefnclass not implemented for Twelf"; ""
- 936 |   | Lex _ | Menhir _ -> ""
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "defns.ml", line 1058, characters 32-46:
- 1058 |             let cc = Char.code (Char.lowercase c) in
-                                        ^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.Char.lowercase
- Use Char.lowercase_ascii instead.
- File "defns.ml", line 1062, characters 32-46:
- 1062 |             let cc = Char.code (Char.lowercase c) in
-                                        ^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.Char.lowercase
- Use Char.lowercase_ascii instead.
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I ../ocamlgraph-1.7 -c ln_transform.ml
- File "ln_transform.ml", lines 1057-1067, characters 4-7:
- 1057 | ....match mse with
- 1058 |     | Empty -> 
- 1059 | 	"0",[]
- 1060 |     | MetaVarExp mv -> 
- 1061 | 	"1",[] (* FZ is this correct in the general case? *)
- ...
- 1064 |     | Aux (f1,nt1) -> 
- 1065 | 	let name = arity_name f1 (Auxl.promote_ntr xd_transformed (Auxl.primary_ntr_of_ntr xd_transformed (fst nt1))) in
- 1066 | 	name ^ " " ^ Grammar_pp.pp_nonterm m xd_transformed nt1,
- 1067 | 	[name]
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (NonTermExp _|MetaVarListExp (_, _)|NonTermListExp (_, _)|AuxList (_, _, _))
- ocamlc -g -dtypes   -I ../ocamlgraph-1.7 -c coq_induct.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I ../ocamlgraph-1.7 -c coq_induct.ml
- ocamlc -g -dtypes   -I ../ocamlgraph-1.7 -c system_pp.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I ../ocamlgraph-1.7 -c system_pp.ml
- File "system_pp.ml", lines 75-82, characters 4-73:
- 75 | ....( match m with
- 76 |     | Isa io -> fst (!(io.isa_library))
- 77 |     | Hol ho -> fst (!(ho.hol_library))
- 78 |     | Lem lo -> fst (!(lo.lem_library))
- 79 |     | Coq co -> fst (!(co.coq_library))
- 80 |     | Twf wo -> fst (!(wo.twf_library))
- 81 |     | Caml oo-> fst (!(oo.caml_library))
- 82 |     | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_functions")...
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "system_pp.ml", lines 149-156, characters 4-76:
- 149 | ....( match m with
- 150 |     | Isa io -> fst (!(io.isa_library))
- 151 |     | Hol ho -> fst (!(ho.hol_library))
- 152 |     | Lem lo -> fst (!(lo.lem_library))
- 153 |     | Coq co -> fst (!(co.coq_library))
- 154 |     | Twf wo -> fst (!(wo.twf_library))
- 155 |     | Caml oo ->fst (!(oo.caml_library))
- 156 |     | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.errorm m  "pp_functions\n")...
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- File "system_pp.ml", lines 368-420, characters 2-71:
- 368 | ..match m with
- 369 |   | Isa io ->
- 370 |       let imports = 
- 371 |         if Auxl.require_nominal sd.syntax
- 372 |         then "\"/~~/src/HOL/Nominal/Nominal\"" :: sd.syntax.xd_isa_imports
- ...
- 417 |   | Lem lo ->
- 418 |       Printf.fprintf fd "(* generated by Ott %s from: %s *)\n" Version.n sd.sources;
- 419 |       pp_systemdefn_core fd m sd lookup
- 420 |   | Ascii _ | Lex _ | Menhir _ | Tex _ -> Auxl.errorm m "pp_systemdefn"
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- Rdx _
- ocamlc -g -dtypes   -I ../ocamlgraph-1.7 -c lex_menhir_pp.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I ../ocamlgraph-1.7 -c lex_menhir_pp.ml
- File "lex_menhir_pp.ml", lines 269-278, characters 10-11:
- 269 | ..........(match ocamllex_hom_opt, ocamllex_remove_hom with
- 270 |           | Some ocamllex_hom, false -> 
- 271 |               Some (token_name_of mvd.mvd_name, mvd.mvd_name, TK_metavar(ocaml_type, Some ocamllex_hom))
- 272 |           | None, false -> 
- 273 |               Auxl.error ("ocamllex output: no ocamllex or ocamllex-remove hom for "^mvd.mvd_name^"\n")
- 274 |           | Some ocamllex_hom, false -> 
- 275 |               Auxl.error ("ocamllex output: both ocamllex and ocamllex-remove hom for "^mvd.mvd_name^"\n")
- 276 |           | None, true -> 
- 277 |               Some (token_name_of mvd.mvd_name, mvd.mvd_name, TK_metavar(ocaml_type, None))
- 278 |           )
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- (Some _, true)
- File "lex_menhir_pp.ml", line 274, characters 12-36:
- 274 |           | Some ocamllex_hom, false -> 
-                   ^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 11: this match case is unused.
- File "lex_menhir_pp.ml", line 543, characters 2-19:
- 543 |   String.capitalize p.prod_name 
-         ^^^^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.String.capitalize
- Use String.capitalize_ascii instead.
- File "lex_menhir_pp.ml", line 562, characters 78-95:
- 562 |     let aux_prod_name = (if r.rule_pn_wrapper<>"" then r.rule_pn_wrapper else String.capitalize r.rule_ntr_name ^"_") ^ "aux" in
-                                                                                     ^^^^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.String.capitalize
- Use String.capitalize_ascii instead.
- File "lex_menhir_pp.ml", line 587, characters 4-21:
- 587 |     String.capitalize p.prod_name 
-           ^^^^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.String.capitalize
- Use String.capitalize_ascii instead.
- File "lex_menhir_pp.ml", line 787, characters 20-37:
- 787 |       "string \"" ^ String.capitalize p.prod_name ^ "\"" 
-                           ^^^^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.String.capitalize
- Use String.capitalize_ascii instead.
- ocamlc -g -dtypes   -I ../ocamlgraph-1.7 -c align.mli
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I ../ocamlgraph-1.7 -c align.ml
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -I ../ocamlgraph-1.7 -c main.ml
- File "main.ml", line 448, characters 13-30:
- 448 |     | [n] -> String.capitalize (Filename.chop_extension n)
-                    ^^^^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.String.capitalize
- Use String.capitalize_ascii instead.
- File "main.ml", line 467, characters 13-30:
- 467 |     | [n] -> String.capitalize (Filename.chop_extension n)
-                    ^^^^^^^^^^^^^^^^^
- Alert deprecated: Stdlib.String.capitalize
- Use String.capitalize_ascii instead.
- sed -e 's/__VERSION__/0.27/' \
-     -e '/__DATE__/r tmp_date.txt' \
-     -e '/__DATE__/d' <version_src.tex >version.tex
- echo Makefile location.cmx types.cmx auxl.cmx merge.cmx global_option.cmx grammar_lexer.cmx grammar_parser.cmx version.cmx grammar_pp.cmx parse_table.cmx glr.cmx new_term_parser.cmx term_parser.cmx dependency.cmx bounds.cmx context_pp.cmx quotient_rules.cmx grammar_typecheck.cmx transform.cmx substs_pp.cmx subrules_pp.cmx embed_pp.cmx defns.cmx ln_transform.cmx coq_induct.cmx system_pp.cmx lex_menhir_pp.cmx align.cmx main.cmx align.cmi bounds.cmi coq_induct.cmi defns.cmi dependency.cmi embed_pp.cmi grammar_typecheck.cmi merge.cmi subrules_pp.cmi substs_pp.cmi system_pp.cmi lex_menhir_pp.cmi transform.cmi term_parser.cmi version.tex
- Makefile location.cmx types.cmx auxl.cmx merge.cmx global_option.cmx grammar_lexer.cmx grammar_parser.cmx version.cmx grammar_pp.cmx parse_table.cmx glr.cmx new_term_parser.cmx term_parser.cmx dependency.cmx bounds.cmx context_pp.cmx quotient_rules.cmx grammar_typecheck.cmx transform.cmx substs_pp.cmx subrules_pp.cmx embed_pp.cmx defns.cmx ln_transform.cmx coq_induct.cmx system_pp.cmx lex_menhir_pp.cmx align.cmx main.cmx align.cmi bounds.cmi coq_induct.cmi defns.cmi dependency.cmi embed_pp.cmi grammar_typecheck.cmi merge.cmi subrules_pp.cmi substs_pp.cmi system_pp.cmi lex_menhir_pp.cmi transform.cmi term_parser.cmi version.tex
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -v
- The OCaml native-code compiler, version 4.10.2
- Standard library directory: /home/opam/.opam/4.10/lib/ocaml
- ocamlopt -w y -g -dtypes -unsafe -inline 9 -o ott.opt str.cmxa ../ocamlgraph-1.7/graph.cmxa  location.cmx  types.cmx  auxl.cmx  merge.cmx  global_option.cmx  grammar_lexer.cmx  grammar_parser.cmx  version.cmx  grammar_pp.cmx  parse_table.cmx  glr.cmx  new_term_parser.cmx  term_parser.cmx  dependency.cmx  bounds.cmx  context_pp.cmx  quotient_rules.cmx  grammar_typecheck.cmx  transform.cmx  substs_pp.cmx  subrules_pp.cmx  embed_pp.cmx  defns.cmx  ln_transform.cmx  coq_induct.cmx  system_pp.cmx  lex_menhir_pp.cmx  align.cmx  main.cmx
- ln -s -f ott.opt ott
- make[2]: Leaving directory '/home/opam/.opam/4.10/.opam-switch/build/ott.0.27/src'
- cp ./ott ../bin/ott
- make[1]: Leaving directory '/home/opam/.opam/4.10/.opam-switch/build/ott.0.27/src'
-> compiled  ott.0.27
-> installed ott.0.27
Done.
# Run eval $(opam env) to update the current shell environment
2024-02-15 06:49.36 ---> saved as "0f80e5e06bb4b21d1e9c449e4aafc4c42e888c8bb4eee98b1516d4a36157f58c"
Job succeeded