From 3c6679676c3963b7c3ec7c1eadbf24ae70311408 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 14 Jul 2017 15:43:40 +0200 Subject: 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. --- interp/declare.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'interp') 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; -- cgit v1.2.3