diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 4 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 5 |
2 files changed, 4 insertions, 5 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index a9de01bfd0..5f7eb78a40 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -866,7 +866,7 @@ let explain_unsatisfiable_constraints env sigma constr comp = let info = Evar.Map.find ev undef in explain_typeclass_resolution env sigma info k ++ fnl () ++ cstr -let explain_pretype_error env sigma err = +let rec explain_pretype_error env sigma err = let env = Evardefine.env_nf_betaiotaevar sigma env in let env = make_all_name_different env sigma in match err with @@ -893,7 +893,7 @@ let explain_pretype_error env sigma err = | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env sigma m n | CannotFindWellTypedAbstraction (p,l,e) -> explain_cannot_find_well_typed_abstraction env sigma p l - (Option.map (fun (env',e) -> explain_type_error env' sigma e) e) + (Option.map (fun (env',e) -> explain_pretype_error env' sigma e) e) | WrongAbstractionType (n,a,t,u) -> explain_wrong_abstraction_type env sigma n a t u | AbstractionOverMeta (m,n) -> explain_abstraction_over_meta env m n diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index f972e05d3b..e9cd4272e6 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -524,8 +524,7 @@ let pr_record_field (x, { rf_subclass = oc ; rf_priority = pri ; rf_notation = n prx ++ prpri ++ prlist (pr_decl_notation @@ pr_constr) ntn let pr_record_decl c fs = - pr_opt pr_lident c ++ (if c = None then str"{" else str" {") ++ - hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}") + pr_opt pr_lident c ++ pr_record "{" "}" pr_record_field fs let pr_printable = function | PrintFullContext -> @@ -966,7 +965,7 @@ let pr_vernac_expr v = str":" ++ spc () ++ pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++ (match props with - | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}" + | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ pr_record_body "{" "}" pr_lconstr l | Some (true,_) -> assert false | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p | None -> mt())) |