diff options
| author | Matthieu Sozeau | 2014-06-17 14:15:08 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-17 15:42:14 +0200 |
| commit | d104b50b9c9a589d9fd8e44bdf56794c8aea4e53 (patch) | |
| tree | d68e8fc7f40dc25d075923b3df635c25e650d2a0 /toplevel | |
| parent | b8834d66013b38cef247507f312bb081de04da27 (diff) | |
Safer entry point of primitive projections in the kernel, now it does recognize
a projection constant only of the form
λ params (r : I params), match r with BuildR args => args_i end, without any
other user input and relies on it being typable (no more primitive projections
escaping this).
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/ind_tables.ml | 2 | ||||
| -rw-r--r-- | toplevel/indschemes.ml | 2 | ||||
| -rw-r--r-- | toplevel/obligations.ml | 2 | ||||
| -rw-r--r-- | toplevel/record.ml | 11 |
4 files changed, 7 insertions, 10 deletions
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 1f09d76205..6f3f5cc49b 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -126,7 +126,7 @@ let define internal id c p univs = const_entry_body = Future.from_val ((c,Univ.ContextSet.empty), Declareops.no_seff); const_entry_secctx = None; const_entry_type = None; - const_entry_proj = None; + const_entry_proj = false; const_entry_polymorphic = p; const_entry_universes = Evd.evar_context_universe_context ctx; const_entry_opaque = false; diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index a5e30b210f..d17136f1c8 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -120,7 +120,7 @@ let define id internal ctx c t = { const_entry_body = c; const_entry_secctx = None; const_entry_type = t; - const_entry_proj = None; + const_entry_proj = false; const_entry_polymorphic = true; const_entry_universes = Evd.universe_context ctx; const_entry_opaque = false; diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 1543c5e875..067b925540 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -636,7 +636,7 @@ let declare_obligation prg obl body uctx = { const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Declareops.no_seff); const_entry_secctx = None; const_entry_type = if List.is_empty ctx then Some ty else None; - const_entry_proj = None; + const_entry_proj = false; const_entry_polymorphic = poly; const_entry_universes = uctx; const_entry_opaque = opaque; diff --git a/toplevel/record.ml b/toplevel/record.ml index 71f0175985..4b8a4fa0d2 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -247,12 +247,9 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in let kn = try - let projinfo = - (fst indsp, mib.mind_nparams, nfields - nfi, ccl) - in - let projinfo = - if !primitive_flag && optci = None then Some projinfo - else None + let makeprim = + if !primitive_flag && optci = None then true + else false in let cie = { const_entry_body = @@ -261,7 +258,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls const_entry_type = Some projtyp; const_entry_polymorphic = poly; const_entry_universes = ctx; - const_entry_proj = projinfo; + const_entry_proj = makeprim; const_entry_opaque = false; const_entry_inline_code = false; const_entry_feedback = None; |