diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-14 15:43:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-26 15:11:33 +0200 |
| commit | 3c6679676c3963b7c3ec7c1eadbf24ae70311408 (patch) | |
| tree | 1de23a7b0802e899d2bf3d8f189f31f7f8e0f745 /interp/declare.ml | |
| parent | 9961577dfbb93f0b691c355ba99822665def037f (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/declare.ml')
| -rw-r--r-- | interp/declare.ml | 6 |
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; |