diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/assumptions.mli | 2 | ||||
| -rw-r--r-- | vernac/classes.mli | 4 | ||||
| -rw-r--r-- | vernac/comFixpoint.mli | 4 | ||||
| -rw-r--r-- | vernac/himsg.mli | 2 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 30 | ||||
| -rw-r--r-- | vernac/obligations.ml | 2 | ||||
| -rw-r--r-- | vernac/record.mli | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 14 |
8 files changed, 38 insertions, 22 deletions
diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli index 0e2b0c80e8..751e79d89c 100644 --- a/vernac/assumptions.mli +++ b/vernac/assumptions.mli @@ -23,7 +23,7 @@ open Printer val traverse : Label.t -> constr -> (Refset_env.t * Refset_env.t Refmap_env.t * - (Label.t * Context.Rel.t * types) list Refmap_env.t) + (Label.t * Constr.rel_context * types) list Refmap_env.t) (** Collects all the assumptions (optionally including opaque definitions) on which a term relies (together with their type). The above warning of diff --git a/vernac/classes.mli b/vernac/classes.mli index bd30b2d60e..9c37364cb0 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -16,9 +16,9 @@ open Libnames (** Errors *) -val mismatched_params : env -> constr_expr list -> Context.Rel.t -> 'a +val mismatched_params : env -> constr_expr list -> Constr.rel_context -> 'a -val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a +val mismatched_props : env -> constr_expr list -> Constr.rel_context -> 'a (** Instance declaration *) diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index f51bfbad59..b1a9c8a5a3 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -82,12 +82,12 @@ val interp_fixpoint : val declare_fixpoint : locality -> polymorphic -> recursive_preentry * UState.universe_decl * UState.t * - (Context.Rel.t * Impargs.manual_implicits * int option) list -> + (Constr.rel_context * Impargs.manual_implicits * int option) list -> Proof_global.lemma_possible_guards -> decl_notation list -> unit val declare_cofixpoint : locality -> polymorphic -> recursive_preentry * UState.universe_decl * UState.t * - (Context.Rel.t * Impargs.manual_implicits * int option) list -> + (Constr.rel_context * Impargs.manual_implicits * int option) list -> decl_notation list -> unit (** Very private function, do not use *) diff --git a/vernac/himsg.mli b/vernac/himsg.mli index 1d38075022..91caddcf13 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -25,7 +25,7 @@ val explain_pretype_error : env -> Evd.evar_map -> pretype_error -> Pp.t val explain_inductive_error : inductive_error -> Pp.t -val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Context.Rel.t -> Pp.t +val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Constr.rel_context -> Pp.t val explain_typeclass_error : env -> typeclass_error -> Pp.t diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index da14358ef5..240147c8d9 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -487,6 +487,15 @@ and check_no_ldots_in_box = function let error_not_same ?loc () = user_err ?loc Pp.(str "The format is not the same on the right- and left-hand sides of the special token \"..\".") +let find_prod_list_loc sfmt fmt = + (* [fmt] is some [UnpTerminal x :: sfmt @ UnpTerminal ".." :: sfmt @ UnpTerminal y :: rest] *) + if List.is_empty sfmt then + (* No separators; we highlight the sequence "x .." *) + Loc.merge_opt (fst (List.hd fmt)) (fst (List.hd (List.tl fmt))) + else + (* A separator; we highlight the separating sequence *) + Loc.merge_opt (fst (List.hd sfmt)) (fst (List.last sfmt)) + let skip_var_in_recursive_format = function | (_,UnpTerminal s) :: sl (* skip first var *) when not (List.for_all (fun c -> c = " ") (String.explode s)) -> (* To do, though not so important: check that the names match @@ -496,6 +505,8 @@ let skip_var_in_recursive_format = function | [] -> assert false let read_recursive_format sl fmt = + (* Turn [[UnpTerminal s :: some-list @ UnpTerminal ".." :: same-some-list @ UnpTerminal s' :: rest] *) + (* into [(some-list,rest)] *) let get_head fmt = let sl = skip_var_in_recursive_format fmt in try split_format_at_ldots [] sl with Exit -> error_not_same ?loc:(fst (List.last (if sl = [] then fmt else sl))) () in @@ -528,10 +539,10 @@ let hunks_of_format (from,(vars,typs)) symfmt = let i = index_id m vars in let typ = List.nth typs (i-1) in let _,prec = precedence_of_entry_type from typ in - let slfmt,fmt = read_recursive_format sl fmt in - let sl, slfmt = aux (sl,slfmt) in - if not (List.is_empty sl) then error_format ?loc:(fst (List.last fmt)) (); - let symbs, l = aux (symbs,fmt) in + let loc_slfmt,rfmt = read_recursive_format sl fmt in + let sl, slfmt = aux (sl,loc_slfmt) in + if not (List.is_empty sl) then error_format ?loc:(find_prod_list_loc loc_slfmt fmt) (); + let symbs, l = aux (symbs,rfmt) in let hunk = match typ with | ETConstr _ -> UnpListMetaVar (i,prec,slfmt) | ETBinder isopen -> @@ -1312,8 +1323,15 @@ let make_pa_rule level (typs,symbols) ntn need_squash = let make_pp_rule level (typs,symbols) fmt = match fmt with - | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols level)] - | Some fmt -> hunks_of_format (level, List.split typs) (symbols, parse_format fmt) + | None -> + let hunks = make_hunks typs symbols level in + if List.exists (function _,(UnpCut (PpBrk _) | UnpListMetaVar _) -> true | _ -> false) hunks then + [UnpBox (PpHOVB 0,hunks)] + else + (* Optimization to work around what seems an ocaml Format bug (see Mantis #7804/#7807) *) + List.map snd hunks (* drop locations which are dummy *) + | Some fmt -> + hunks_of_format (level, List.split typs) (symbols, parse_format fmt) (* let make_syntax_rules i_typs (ntn,prec,need_squash) sy_data fmt extra onlyprint compat = *) let make_syntax_rules (sd : SynData.syn_data) = let open SynData in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index fa6a9adf1b..1f401b4e15 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -40,7 +40,7 @@ let check_evars env evm = type oblinfo = { ev_name: int * Id.t; - ev_hyps: Context.Named.t; + ev_hyps: Constr.named_context; ev_status: bool * Evar_kinds.obligation_definition_status; ev_chop: int option; ev_src: Evar_kinds.t Loc.located; diff --git a/vernac/record.mli b/vernac/record.mli index 7cf7da1e2d..567f2b3138 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -22,7 +22,7 @@ val declare_projections : bool list -> UnivNames.universe_binders -> Impargs.manual_implicits list -> - Context.Rel.t -> + Constr.rel_context -> (Name.t * bool) list * Constant.t option list val definition_structure : diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 43c974846d..6d1abeca16 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -263,15 +263,13 @@ let print_namespace ns = let matches mp = match match_modulepath ns mp with | Some [] -> true | _ -> false in - let constants = (Global.env ()).Environ.env_globals.Environ.env_constants in let constants_in_namespace = - Cmap_env.fold (fun c (body,_) acc -> - let kn = Constant.user c in - if matches (KerName.modpath kn) then - acc++fnl()++hov 2 (print_constant kn body) - else - acc - ) constants (str"") + Environ.fold_constants (fun c body acc -> + let kn = Constant.user c in + if matches (KerName.modpath kn) + then acc++fnl()++hov 2 (print_constant kn body) + else acc) + (Global.env ()) (str"") in (print_list Id.print ns)++str":"++fnl()++constants_in_namespace |