aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/plugin
diff options
context:
space:
mode:
authorEnrico Tassi2016-02-03 18:22:08 +0100
committerEnrico Tassi2016-02-03 18:22:08 +0100
commit141d8bd469e0b31d36a3b3f3f90eda8ad4a23a7d (patch)
treee0f5b1351384d8e95f3a1ced5a7a3eeac1a5dba5 /mathcomp/ssreflect/plugin
parent3cc0493b8b8b6eba59655855e4e5dadd335563c0 (diff)
Register flag "SsrHave NoTCResolution" in the Summary (fix #6)
Diffstat (limited to 'mathcomp/ssreflect/plugin')
-rw-r--r--mathcomp/ssreflect/plugin/trunk/ssreflect.ml42
-rw-r--r--mathcomp/ssreflect/plugin/v8.5/ssreflect.ml42
2 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index 72efb36..b50635c 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
@@ -475,7 +475,7 @@ let _ =
Goptions.optdepr = false;
Goptions.optwrite = (fun b -> ssroldreworder := b) }
-let ssrhaveNOtcresolution = ref false
+let ssrhaveNOtcresolution = Summary.ref ~name:"SSR:havenotcresolution" false
let inHaveTCResolution = Libobject.declare_object {
(Libobject.default_object "SSRHAVETCRESOLUTION") with
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
index eb21fc2..2b958b5 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
@@ -474,7 +474,7 @@ let _ =
Goptions.optdepr = false;
Goptions.optwrite = (fun b -> ssroldreworder := b) }
-let ssrhaveNOtcresolution = ref false
+let ssrhaveNOtcresolution = Summary.ref ~name:"SSR:havenotcresolution" false
let inHaveTCResolution = Libobject.declare_object {
(Libobject.default_object "SSRHAVETCRESOLUTION") with