diff options
| author |  Jasper Hugunin <jasperh@cs.washington.edu> | 2018-06-04 15:47:28 -0700 |
|---|---|---|
| committer | Jasper Hugunin <jasperh@cs.washington.edu> | 2018-07-01 15:42:25 -0700 |
| commit | 313e6bed17b400d638401a5c6e5d442eadb73d3a (patch) | |
| tree | 494b64ac86538e07216c5da59315168688935c6f /vernac/vernacentries.ml | |
| parent | 033c32a32fedcf2160bb38a3fed55efa9d1c2b77 (diff) | |
Implement uniform parameters in ComInductive
Don't allow notations attached to uniform inductives
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 6d1abeca1..e76921d1d 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -537,6 +537,8 @@ let should_treat_as_cumulative cum poly = else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.") | None -> poly && Flags.is_polymorphic_inductive_cumulativity () +let should_treat_as_uniform () = ComInductive.NonUniformParameters (* TODO: Add a flag *) + let vernac_record cum k poly finite records = let is_cumulative = should_treat_as_cumulative cum poly in let map ((coe, (id, pl)), binders, sort, nameopt, cfs) = @@ -642,7 +644,8 @@ let vernac_inductive ~atts cum lo finite indl = in let indl = List.map unpack indl in let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in - ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo finite + let uniform = should_treat_as_uniform () in + ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo ~uniform finite else user_err (str "Mixed record-inductive definitions are not allowed") (* @@ -2089,7 +2092,7 @@ let interp ?proof ~atts ~st c = | VernacExactProof c -> vernac_exact_proof c | VernacAssumption ((discharge,kind),nl,l) -> vernac_assumption ~atts discharge kind l nl - | VernacInductive (cum, priv,finite,l) -> vernac_inductive ~atts cum priv finite l + | VernacInductive (cum, priv, finite, l) -> vernac_inductive ~atts cum priv finite l | VernacFixpoint (discharge, l) -> vernac_fixpoint ~atts discharge l | VernacCoFixpoint (discharge, l) -> vernac_cofixpoint ~atts discharge l | VernacScheme l -> vernac_scheme l |