diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-15 16:05:03 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-15 16:05:03 +0000 |
| commit | 66139b2e1f66b826dd5dbdb8a9ade64a4d5e11c6 (patch) | |
| tree | 3224a1c72541eb786d6c927fbaab51a44481ce38 /checker/declarations.ml | |
| parent | 07c80f246315ac314c82d580bf356df3fb8201d8 (diff) | |
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
Diffstat (limited to 'checker/declarations.ml')
| -rw-r--r-- | checker/declarations.ml | 17 |
1 files changed, 4 insertions, 13 deletions
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 *) |