diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/assumptions.ml | 2 | ||||
| -rw-r--r-- | vernac/auto_ind_decl.ml | 2 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 7 | ||||
| -rw-r--r-- | vernac/himsg.ml | 3 |
4 files changed, 7 insertions, 7 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 0bcd3c64eb..b000745961 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -71,7 +71,7 @@ let rec fields_of_functor f subs mp0 args = function let rec lookup_module_in_impl mp = match mp with | MPfile _ -> Global.lookup_module mp - | MPbound _ -> assert false + | MPbound _ -> Global.lookup_module mp | MPdot (mp',lab') -> if ModPath.equal mp' (Global.current_modpath ()) then Global.lookup_module mp diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index e33aa38173..3bf3925b4b 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -543,7 +543,7 @@ let eqI ind l = and e, eff = try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff with Not_found -> user_err ~hdr:"AutoIndDecl.eqI" - (str "The boolean equality on " ++ MutInd.print (fst ind) ++ str " is needed."); + (str "The boolean equality on " ++ Printer.pr_inductive (Global.env ()) ind ++ str " is needed."); in (if Array.equal Constr.equal eA [||] then e else mkApp(e,eA)), eff (**********************************************************************) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 650b28ea67..7dd5471f3f 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -83,11 +83,10 @@ GRAMMAR EXTEND Gram ] ; decorated_vernac: - [ [ a = attributes ; fv = vernac -> { let (f, v) = fv in (List.append a f, v) } - | fv = vernac -> { fv } ] - ] + [ [ a = LIST0 quoted_attributes ; fv = vernac -> + { let (f, v) = fv in (List.append (List.flatten a) f, v) } ] ] ; - attributes: + quoted_attributes: [ [ "#[" ; a = attribute_list ; "]" -> { a } ] ] ; diff --git a/vernac/himsg.ml b/vernac/himsg.ml index e7b2a0e8a6..71155d7921 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -896,7 +896,8 @@ let explain_not_match_error = function quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t2) | IncompatibleConstraints cst -> str " the expected (polymorphic) constraints do not imply " ++ - let cst = Univ.AUContext.instantiate (Univ.AUContext.instance cst) cst in + let cst = Univ.UContext.constraints (Univ.AUContext.repr cst) in + (** FIXME: provide a proper naming for the bound variables *) quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst) let explain_signature_mismatch l spec why = |