diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/explainErr.ml | 1 | ||||
| -rw-r--r-- | vernac/obligations.ml | 8 | ||||
| -rw-r--r-- | vernac/record.ml | 8 |
3 files changed, 11 insertions, 6 deletions
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index 71770a21ca..42b313f200 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -28,7 +28,6 @@ exception EvaluatedError of Pp.t * exn option let explain_exn_default = function (* Basic interaction exceptions *) | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") - | Gramlib.Plexing.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") | CLexer.Error.E err -> hov 0 (str (CLexer.Error.to_string err)) | Sys_error msg -> hov 0 (str "System error: " ++ guill msg) | Out_of_memory -> hov 0 (str "Out of memory.") diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 6642d04c98..b4dd7d06b5 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -921,15 +921,15 @@ let obligation_hook prg obl num auto ctx' _ gr = | (true, Evar_kinds.Define true) -> if not transparent then err_not_transp () | _ -> () -in + in let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in let inst, ctx' = if not (pi2 prg.prg_kind) (* Not polymorphic *) then (* The universe context was declared globally, we continue from the new global environment. *) - let evd = Evd.from_env (Global.env ()) in - let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in - Univ.Instance.empty, Evd.evar_universe_context ctx' + let ctx = UState.make (Global.universes ()) in + let ctx' = UState.merge_subst ctx (UState.subst ctx') in + Univ.Instance.empty, ctx' else (* We get the right order somehow, but surely it could be enforced in a clearer way. *) let uctx = UState.context ctx' in diff --git a/vernac/record.ml b/vernac/record.ml index 1b7b828f47..ed5edb7e3b 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -414,9 +414,15 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St mind_entry_lc = [type_constructor] } in let blocks = List.mapi mk_block record_data in + let primitive = + !primitive_flag && + List.for_all (fun (_,_,_,_,fields,_,_) -> List.exists is_local_assum fields) record_data + (* will warn_non_primitive_record in declare_projections if we try + to declare a 0-field record *) + in let mie = { mind_entry_params = params; - mind_entry_record = Some (if !primitive_flag then Some binder_name else None); + mind_entry_record = Some (if primitive then Some binder_name else None); mind_entry_finite = finite; mind_entry_inds = blocks; mind_entry_private = None; |