From 32c83676c96ae4a218de0bec75d2f3353381dfb3 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 28 Aug 2014 19:49:16 +0200 Subject: Change the way primitive projections are declared to the kernel. Now kernel/indtypes builds the corresponding terms (has to be trusted) while translate_constant just binds a constant name to the already entered projection body, avoiding the dubious "check" of user given terms. "case" Pattern-matching on primitive records is now disallowed, and the default scheme is implemented using projections and eta (all elimination tactics now use projections as well). Elaborate "let (x, y) := p in t" using let bindings for the projections of p too. --- kernel/cooking.ml | 3 +++ 1 file changed, 3 insertions(+) (limited to 'kernel/cooking.ml') diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 3dd782342..2d316fc1d 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -215,6 +215,8 @@ let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } = in let projection pb = let c' = abstract_constant_body (expmod pb.proj_body) hyps in + let etab = abstract_constant_body (expmod (fst pb.proj_eta)) hyps in + let etat = abstract_constant_body (expmod (snd pb.proj_eta)) hyps in let ((mind, _), _), n' = try let c' = share_univs cache (IndRef (pb.proj_ind,0)) Univ.Instance.empty modlist in @@ -229,6 +231,7 @@ let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } = in let ctx, ty' = decompose_prod_n (n' + pb.proj_npars + 1) typ in { proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg; + proj_eta = etab, etat; proj_type = ty'; proj_body = c' } in let univs = UContext.union abs_ctx univs in -- cgit v1.2.3