diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-09 15:51:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-09 15:51:05 +0200 |
| commit | 8efb78da7900e7f13105aac8361272477f8f5119 (patch) | |
| tree | 6efe7fbf8c847b6e17239aebb7283ff125024def /checker | |
| parent | 3c481b2ef7e7abd813fdac22b4bbe8d89de88141 (diff) | |
| parent | 5ea2539d4a7d12938787a74a12112e76aaf2a4ee (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/check.ml | 2 | ||||
| -rw-r--r-- | checker/checker.ml | 5 |
2 files changed, 2 insertions, 5 deletions
diff --git a/checker/check.ml b/checker/check.ml index 93eb2a0d2..da3cd0316 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -303,7 +303,7 @@ let intern_from_file (dir, f) = try let ch = System.with_magic_number_check raw_intern_library f in let (sd:Cic.summary_disk), _, digest = System.marshal_in_segment f ch in - let (md:Cic.library_disk), _, _ = System.marshal_in_segment f ch in + let (md:Cic.library_disk), _, digest = System.marshal_in_segment f ch in let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in let (discharging:'a option), _, _ = System.marshal_in_segment f ch in let (tasks:'a option), _, _ = System.marshal_in_segment f ch in diff --git a/checker/checker.ml b/checker/checker.ml index 61b13c60b..9d76fb09e 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -179,10 +179,7 @@ let print_usage_channel co command = output_string co command; output_string co "coqchk options are:\n"; output_string co -" -I dir -as coqdir map physical dir to logical coqdir\ -\n -I dir map directory dir to the empty logical path\ -\n -include dir (idem)\ -\n -R dir coqdir recursively map physical dir to logical coqdir\ +" -R dir coqdir map physical dir to logical coqdir\ \n\ \n -admit module load module and dependencies without checking\ \n -norec module check module but admit dependencies without checking\ |