aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-07-14 15:43:40 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-07-26 15:11:33 +0200
commit3c6679676c3963b7c3ec7c1eadbf24ae70311408 (patch)
tree1de23a7b0802e899d2bf3d8f189f31f7f8e0f745 /interp
parent9961577dfbb93f0b691c355ba99822665def037f (diff)
More precise type of entries capturing their lack of side-effects.
We sprinkle a few GADTs in the kernel in order to statically ensure that entries are pure, so that we get stronger invariants.
Diffstat (limited to 'interp')
-rw-r--r--interp/declare.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/interp/declare.ml b/interp/declare.ml
index f95d025e4..8cafb5f3a 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -184,7 +184,7 @@ let discharge_constant ((sp, kn), obj) =
(* Hack to reduce the size of .vo: we keep only what load/open needs *)
let dummy_constant_entry =
ConstantEntry
- (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None))
+ (PureEntry, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None))
let dummy_constant cst = {
cst_decl = dummy_constant_entry;
@@ -220,7 +220,7 @@ let declare_constant_common id cst =
List.iter (fun (c,ce,role) ->
(* handling of private_constants just exported *)
let o = inConstant {
- cst_decl = ConstantEntry (false, ce);
+ cst_decl = ConstantEntry (PureEntry, ce);
cst_hyps = [] ;
cst_kind = IsProof Theorem;
cst_locl = false;
@@ -270,7 +270,7 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
| _ -> false
in
let cst = {
- cst_decl = ConstantEntry (export,cd);
+ cst_decl = ConstantEntry (EffectEntry export,cd);
cst_hyps = [] ;
cst_kind = kind;
cst_locl = local;