aboutsummaryrefslogtreecommitdiff
path: root/checker/values.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-05-03 20:34:41 +0200
committerPierre-Marie Pédrot2020-05-13 12:50:41 +0200
commit3e04d6c024dd03878b0b487cf823f5586d6fd397 (patch)
tree4be4f12a7979e1ed44d44b011feac7f770df81aa /checker/values.ml
parent67f0e9fd40dc2f7b30a8aec4c7efb032e61a001e (diff)
Store the OCaml version used for Coq in vo files.
Diffstat (limited to 'checker/values.ml')
-rw-r--r--checker/values.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/values.ml b/checker/values.ml
index 76e3ab0d45..cce0ce7203 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -435,7 +435,7 @@ let v_stm_seg = v_pair v_tasks v_counters
(** Toplevel structures in a vo (see Cic.mli) *)
let v_libsum =
- Tuple ("summary", [|v_dp;v_deps|])
+ Tuple ("summary", [|v_dp;v_deps;String|])
let v_lib =
Tuple ("library",[|v_compiled_lib;v_libraryobjs|])