From 66139b2e1f66b826dd5dbdb8a9ade64a4d5e11c6 Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 15 Apr 2013 16:05:03 +0000 Subject: Checker: empty sections hardcoded in cb and mind git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16400 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/declarations.ml | 17 ++++------------- 1 file changed, 4 insertions(+), 13 deletions(-) (limited to 'checker/declarations.ml') diff --git a/checker/declarations.ml b/checker/declarations.ml index 886901e1a..58a5f2602 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -491,7 +491,6 @@ let subst_arity sub = function (* NB: we leave bytecode and native code fields untouched *) let subst_const_body sub cb = { cb with - const_hyps = (assert (List.is_empty cb.const_hyps); []); const_body = subst_constant_def sub cb.const_body; const_type = subst_arity sub cb.const_type } @@ -507,7 +506,7 @@ let subst_mind_packet sub mbp = { mind_consnames = mbp.mind_consnames; mind_consnrealdecls = mbp.mind_consnrealdecls; mind_typename = mbp.mind_typename; - mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc; + mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc; mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt; mind_arity = subst_arity sub mbp.mind_arity; mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc; @@ -521,17 +520,9 @@ let subst_mind_packet sub mbp = let subst_mind sub mib = - { mind_record = mib.mind_record ; - mind_finite = mib.mind_finite ; - mind_ntypes = mib.mind_ntypes ; - mind_hyps = (assert (List.is_empty mib.mind_hyps); []) ; - mind_nparams = mib.mind_nparams; - mind_nparams_rec = mib.mind_nparams_rec; - mind_params_ctxt = - map_rel_context (subst_mps sub) mib.mind_params_ctxt; - mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; - mind_constraints = mib.mind_constraints; - mind_native_name = mib.mind_native_name} + { mib with + mind_params_ctxt = map_rel_context (subst_mps sub) mib.mind_params_ctxt; + mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets } (* Modules *) -- cgit v1.2.3