Merge branch 'non-exhaustive-match-in-pdriver-ml' into 'master'

Resolve "non-exhaustive match in pdriver.ml after the ComputerEucildeanDivision merge"

Closes #154

See merge request why3/why3!11

Makefile.in

@@ -94,8 +94,9 @@ INCLUDES = @WHY3INCLUDE@ @ZIPINCLUDE@ @MENHIRINCLUDE@ @NUMINCLUDE@
 #   5    Partially applied function: expression whose result has function
 #        type and is ignored.
 #   48   Implicit elimination of optional arguments.
+#   8    Partial match: missing cases in pattern-matching.
 
-WARNINGS = A-4-9-41-44-45-50-52@5@48
+WARNINGS = A-4-9-41-44-45-50-52@5@8@48
 
 OFLAGS = -w $(WARNINGS) -safe-string -keep-locs -bin-annot -dtypes -g $(INCLUDES)
 BFLAGS = -w $(WARNINGS) -safe-string -keep-locs -bin-annot -dtypes -g $(INCLUDES)

src/mlw/pdriver.ml

@@ -167,6 +167,8 @@ let load_driver env file extra_files =
         in
         let m = lookup_meta s in
         ignore (create_meta m (List.map convert al))
+    | Ruse _ ->
+        Loc.errorm "theory use cannot be used in extraction driver"
   in
   let add_local th (loc,rule) = Loc.try2 ~loc add_local th rule in
   let open Pmodule in