proper error message when missing type parameters

src/driver/driver.ml

@@ -178,7 +178,8 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
     let f,id = let l = List.rev q in List.rev (List.tl l),List.hd l in
     let th =
       try Env.read_theory ~format:"why" env f id
-      with e -> raise (Loc.Located (loc,e))
+      with e when not (Debug.test_flag Debug.stack_trace) -> 
+        raise (Loc.Located (loc,e))
     in
     qualid := q;
     List.iter (add_local th) trl

src/parser/denv.ml

@@ -52,8 +52,12 @@ let tyapp ts tyl = match ts.ts_def with
       Tyapp (ts, tyl)
   | Some ty ->
       let add m v t = Mtv.add v t m in
-      let s = List.fold_left2 add Mtv.empty ts.ts_args tyl in
-      type_inst s ty
+      try
+        let s = List.fold_left2 add Mtv.empty ts.ts_args tyl in
+        type_inst s ty
+      with Invalid_argument _ ->
+        Loc.errorm "this type expects %d parameters" (List.length ts.ts_args)
+
 
 type dty = dty_view