diff options
author | 2010-10-14 17:58:31 +0200 | |
---|---|---|
committer | 2010-10-14 17:58:31 +0200 | |
commit | d06cea3ce4526736b5d32ba1780dbbc87c37c981 (patch) | |
tree | 2c2ea5a4633a41cfd4451e1eefb79c171312c881 /toplevel | |
parent | aae7cec8d7f5048215b7ed06a8e94cb032bfd21a (diff) | |
parent | 8f4d4c66134804bbf2d2fe65c893b68387272d31 (diff) |
Merge commit 'upstream/8.3+dfsg' into experimental/master
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/cerrors.ml | 113 | ||||
-rw-r--r-- | toplevel/cerrors.mli | 8 | ||||
-rw-r--r-- | toplevel/classes.ml | 4 | ||||
-rw-r--r-- | toplevel/himsg.ml | 3 | ||||
-rw-r--r-- | toplevel/ind_tables.ml | 4 | ||||
-rw-r--r-- | toplevel/indschemes.ml | 34 | ||||
-rw-r--r-- | toplevel/record.ml | 9 | ||||
-rw-r--r-- | toplevel/vernac.ml | 11 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 14 | ||||
-rw-r--r-- | toplevel/vernacexpr.ml | 4 |
10 files changed, 108 insertions, 96 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 5828f12d..db2f9ae9 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cerrors.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: cerrors.ml 13431 2010-09-18 08:15:29Z herbelin $ *) open Pp open Util @@ -28,6 +28,8 @@ let guill s = "\""^s^"\"" let where s = if !Flags.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) +exception EvaluatedError of std_ppcmds * exn option + (* assumption : explain_sys_exn does NOT end with a 'FNL anymore! *) let rec explain_exn_default_aux anomaly_string report_fn = function @@ -69,54 +71,6 @@ let rec explain_exn_default_aux anomaly_string report_fn = function hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report_fn ()) | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.") - | Univ.UniverseInconsistency (o,u,v) -> - let msg = - if !Constrextern.print_universes then - spc() ++ str "(cannot enforce" ++ spc() ++ Univ.pr_uni u ++ spc() ++ - str (match o with Univ.Lt -> "<" | Univ.Le -> "<=" | Univ.Eq -> "=") - ++ spc() ++ Univ.pr_uni v ++ str")" - else - mt() in - hov 0 (str "Error: Universe inconsistency" ++ msg ++ str ".") - | TypeError(ctx,te) -> - hov 0 (str "Error:" ++ spc () ++ Himsg.explain_type_error ctx te) - | PretypeError(ctx,te) -> - hov 0 (str "Error:" ++ spc () ++ Himsg.explain_pretype_error ctx te) - | Typeclasses_errors.TypeClassError(env, te) -> - hov 0 (str "Error:" ++ spc () ++ Himsg.explain_typeclass_error env te) - | InductiveError e -> - hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error e) - | RecursionSchemeError e -> - hov 0 (str "Error:" ++ spc () ++ Himsg.explain_recursion_scheme_error e) - | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when Lazy.force s <> mt () -> - explain_exn_default_aux anomaly_string report_fn exc - | Proof_type.LtacLocated (s,exc) -> - hov 0 (Himsg.explain_ltac_call_trace s ++ fnl () - ++ explain_exn_default_aux anomaly_string report_fn exc) - | Cases.PatternMatchingError (env,e) -> - hov 0 - (str "Error:" ++ spc () ++ Himsg.explain_pattern_matching_error env e) - | Tacred.ReductionTacticError e -> - hov 0 (str "Error:" ++ spc () ++ Himsg.explain_reduction_tactic_error e) - | Logic.RefinerError e -> - hov 0 (str "Error:" ++ spc () ++ Himsg.explain_refiner_error e) - | Nametab.GlobalizationError q -> - hov 0 (str "Error:" ++ spc () ++ - str "The reference" ++ spc () ++ Libnames.pr_qualid q ++ - spc () ++ str "was not found" ++ - spc () ++ str "in the current" ++ spc () ++ str "environment.") - | Nametab.GlobalizationConstantError q -> - hov 0 (str "Error:" ++ spc () ++ - str "No constant of this name:" ++ spc () ++ - Libnames.pr_qualid q ++ str ".") - | Refiner.FailError (i,s) -> - hov 0 (str "Error: Tactic failure" ++ - (if Lazy.force s <> mt() then str ":" ++ Lazy.force s else mt ()) ++ - if i=0 then str "." else str " (level " ++ int i ++ str").") - | Stdpp.Exc_located (loc,exc) -> - hov 0 ((if loc = dummy_loc then (mt ()) - else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) - ++ explain_exn_default_aux anomaly_string report_fn exc) | Lexer.Error Illegal_character -> hov 0 (str "Syntax error: Illegal character.") | Lexer.Error Unterminated_comment -> @@ -140,12 +94,69 @@ let rec explain_exn_default_aux anomaly_string report_fn = function else (mt ())) ++ report_fn ()) - | AlreadyDeclared msg -> - hov 0 (msg ++ str ".") + | EvaluatedError (msg,None) -> + msg + | EvaluatedError (msg,Some reraise) -> + msg ++ explain_exn_default_aux anomaly_string report_fn reraise | reraise -> hov 0 (anomaly_string () ++ str "Uncaught exception " ++ str (Printexc.to_string reraise) ++ report_fn ()) +let wrap_vernac_error strm = + EvaluatedError (hov 0 (str "Error:" ++ spc () ++ strm), None) + +let rec process_vernac_interp_error = function + | Univ.UniverseInconsistency (o,u,v) -> + let msg = + if !Constrextern.print_universes then + spc() ++ str "(cannot enforce" ++ spc() ++ Univ.pr_uni u ++ spc() ++ + str (match o with Univ.Lt -> "<" | Univ.Le -> "<=" | Univ.Eq -> "=") + ++ spc() ++ Univ.pr_uni v ++ str")" + else + mt() in + wrap_vernac_error (str "Universe inconsistency" ++ msg ++ str ".") + | TypeError(ctx,te) -> + wrap_vernac_error (Himsg.explain_type_error ctx te) + | PretypeError(ctx,te) -> + wrap_vernac_error (Himsg.explain_pretype_error ctx te) + | Typeclasses_errors.TypeClassError(env, te) -> + wrap_vernac_error (Himsg.explain_typeclass_error env te) + | InductiveError e -> + wrap_vernac_error (Himsg.explain_inductive_error e) + | RecursionSchemeError e -> + wrap_vernac_error (Himsg.explain_recursion_scheme_error e) + | Cases.PatternMatchingError (env,e) -> + wrap_vernac_error (Himsg.explain_pattern_matching_error env e) + | Tacred.ReductionTacticError e -> + wrap_vernac_error (Himsg.explain_reduction_tactic_error e) + | Logic.RefinerError e -> + wrap_vernac_error (Himsg.explain_refiner_error e) + | Nametab.GlobalizationError q -> + wrap_vernac_error + (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++ + spc () ++ str "was not found" ++ + spc () ++ str "in the current" ++ spc () ++ str "environment.") + | Nametab.GlobalizationConstantError q -> + wrap_vernac_error + (str "No constant of this name:" ++ spc () ++ + Libnames.pr_qualid q ++ str ".") + | Refiner.FailError (i,s) -> + EvaluatedError (hov 0 (str "Error: Tactic failure" ++ + (if Lazy.force s <> mt() then str ":" ++ Lazy.force s else mt ()) ++ + if i=0 then str "." else str " (level " ++ int i ++ str")."), + None) + | AlreadyDeclared msg -> + wrap_vernac_error (msg ++ str ".") + | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when Lazy.force s <> mt () -> + process_vernac_interp_error exc + | Proof_type.LtacLocated (s,exc) -> + EvaluatedError (hov 0 (Himsg.explain_ltac_call_trace s ++ fnl()), + Some (process_vernac_interp_error exc)) + | Stdpp.Exc_located (loc,exc) -> + Stdpp.Exc_located (loc,process_vernac_interp_error exc) + | exc -> + exc + let anomaly_string () = str "Anomaly: " let report () = (str "." ++ spc () ++ str "Please report.") diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli index 00316007..31e0e04f 100644 --- a/toplevel/cerrors.mli +++ b/toplevel/cerrors.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: cerrors.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: cerrors.mli 13431 2010-09-18 08:15:29Z herbelin $ i*) (*i*) open Pp @@ -19,10 +19,14 @@ val print_loc : loc -> std_ppcmds val explain_exn : exn -> std_ppcmds -(** Same, but will re-raise all anomalies instead of explaining them *) +(** Precompute errors raised during vernac interpretation *) val explain_exn_no_anomaly : exn -> std_ppcmds +(** Pre-explain a vernac interpretation error *) + +val process_vernac_interp_error : exn -> exn + (** For debugging purpose (?), the explain function can be twicked *) val explain_exn_function : (exn -> std_ppcmds) ref diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 435ddb4d..2d8aabfc 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classes.ml 13332 2010-07-26 22:12:43Z msozeau $ i*) +(*i $Id: classes.ml 13516 2010-10-07 19:09:38Z msozeau $ i*) (*i*) open Names @@ -233,7 +233,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props if rest <> [] then unbound_method env' k.cl_impl (get_id (fst (List.hd rest))) else - Inl (type_ctx_instance evars env' k.cl_props props subst) + Inl (type_ctx_instance evars (push_rel_context ctx' env') k.cl_props props subst) in evars := Evarutil.nf_evar_map !evars; let term, termtype = diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index a080442c..99ca9879 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: himsg.ml 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: himsg.ml 13465 2010-09-24 22:23:07Z herbelin $ *) open Pp open Util @@ -290,6 +290,7 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = pr_ne_context_of (str "In environment") env ++ st ++ str "." ++ fnl () ++ (try (* May fail with unresolved globals. *) + let fixenv = make_all_name_different fixenv in let pvd = pr_lconstr_env fixenv vdefj.(i).uj_val in str"Recursive definition is:" ++ spc () ++ pvd ++ str "." with _ -> mt ()) diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 4e28ccac..c2d5f31d 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ind_tables.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: ind_tables.ml 13392 2010-09-02 12:11:15Z vsiles $ i*) (* File created by Vincent Siles, Oct 2007, extended into a generic support for generation of inductive schemes by Hugo Herbelin, Nov 2009 *) @@ -125,7 +125,7 @@ let define internal id c = const_entry_boxed = Flags.boxed_definitions() }, Decl_kinds.IsDefinition Scheme) in (match internal with - | KernelSilent -> () + | KernelSilent -> () | _-> definition_message id); kn diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 29d7a12c..9031d8a3 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: indschemes.ml 13333 2010-07-27 10:18:30Z vsiles $ *) +(* $Id: indschemes.ml 13396 2010-09-02 16:52:15Z vsiles $ *) (* Created by Hugo Herbelin from contents related to inductive schemes initially developed by Christine Paulin (induction schemes), Vincent @@ -123,8 +123,8 @@ let declare_beq_scheme_gen internal names kn = let alarm what internal msg = let debug = false in - (* TODO: specify even more by distinguish KernelVerbose and UserVerbose *) match internal with + | KernelVerbose | KernelSilent -> (if debug then Flags.if_verbose Pp.msg_warning @@ -172,17 +172,15 @@ let beq_scheme_msg mind = let declare_beq_scheme_with l kn = try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserVerbose l kn -(* TODO : maybe switch to KernelVerbose to have the right behaviour *) let try_declare_beq_scheme kn = (* TODO: handle Fix, see e.g. TheoryList.In_spec, eventually handle proof-irrelevance; improve decidability by depending on decidability for the parameters rather than on the bl and lb properties *) - try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen KernelSilent [] kn + try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen KernelVerbose [] kn let declare_beq_scheme = declare_beq_scheme_with [] (* Case analysis schemes *) -(* TODO: maybe switch to KernelVerbose *) let declare_one_case_analysis_scheme ind = let (mib,mip) = Global.lookup_inductive ind in let kind = inductive_sort_family mip in @@ -192,7 +190,7 @@ let declare_one_case_analysis_scheme ind = induction scheme, the other ones share the same code with the apropriate type *) if List.mem InType kelim then - ignore (define_individual_scheme dep KernelSilent None ind) + ignore (define_individual_scheme dep KernelVerbose None ind) (* Induction/recursion schemes *) @@ -206,7 +204,6 @@ let kinds_from_type = InProp,ind_dep_scheme_kind_from_type; InSet,rec_dep_scheme_kind_from_type] - (* TODO: maybe switch to kernel verbose *) let declare_one_induction_scheme ind = let (mib,mip) = Global.lookup_inductive ind in let kind = inductive_sort_family mip in @@ -216,7 +213,7 @@ let declare_one_induction_scheme ind = list_map_filter (fun (sort,kind) -> if List.mem sort kelim then Some kind else None) (if from_prop then kinds_from_prop else kinds_from_type) in - List.iter (fun kind -> ignore (define_individual_scheme kind KernelSilent None ind)) + List.iter (fun kind -> ignore (define_individual_scheme kind KernelVerbose None ind)) elims let declare_induction_schemes kn = @@ -241,10 +238,9 @@ let declare_eq_decidability_scheme_with l kn = try_declare_scheme (eq_dec_scheme_msg (kn,0)) declare_eq_decidability_gen UserVerbose l kn -(* TODO: maybe switch to kernel verbose *) let try_declare_eq_decidability kn = try_declare_scheme (eq_dec_scheme_msg (kn,0)) - declare_eq_decidability_gen KernelSilent [] kn + declare_eq_decidability_gen KernelVerbose [] kn let declare_eq_decidability = declare_eq_decidability_scheme_with [] @@ -252,36 +248,34 @@ let ignore_error f x = try ignore (f x) with _ -> () let declare_rewriting_schemes ind = if Hipattern.is_inductive_equality ind then begin - ignore (define_individual_scheme rew_r2l_scheme_kind KernelSilent None ind); - ignore (define_individual_scheme rew_r2l_dep_scheme_kind KernelSilent None ind); + ignore (define_individual_scheme rew_r2l_scheme_kind KernelVerbose None ind); + ignore (define_individual_scheme rew_r2l_dep_scheme_kind KernelVerbose None ind); ignore (define_individual_scheme rew_r2l_forward_dep_scheme_kind - KernelSilent None ind); + KernelVerbose None ind); (* These ones expect the equality to be symmetric; the first one also *) (* needs eq *) - ignore_error (define_individual_scheme rew_l2r_scheme_kind KernelSilent None) ind; + ignore_error (define_individual_scheme rew_l2r_scheme_kind KernelVerbose None) ind; ignore_error - (define_individual_scheme rew_l2r_dep_scheme_kind KernelSilent None) ind; + (define_individual_scheme rew_l2r_dep_scheme_kind KernelVerbose None) ind; ignore_error - (define_individual_scheme rew_l2r_forward_dep_scheme_kind KernelSilent None) ind + (define_individual_scheme rew_l2r_forward_dep_scheme_kind KernelVerbose None) ind end -(* TODO: maybe switch to kernel verbose *) let declare_congr_scheme ind = if Hipattern.is_equality_type (mkInd ind) then begin if try Coqlib.check_required_library Coqlib.logic_module_name; true with _ -> false then - ignore (define_individual_scheme congr_scheme_kind KernelSilent None ind) + ignore (define_individual_scheme congr_scheme_kind KernelVerbose None ind) else warning "Cannot build congruence scheme because eq is not found" end -(* TODO: maybe switch to kernel verbose *) let declare_sym_scheme ind = if Hipattern.is_inductive_equality ind then (* Expect the equality to be symmetric *) - ignore_error (define_individual_scheme sym_scheme_kind KernelSilent None) ind + ignore_error (define_individual_scheme sym_scheme_kind KernelVerbose None) ind (* Scheme command *) diff --git a/toplevel/record.ml b/toplevel/record.ml index cd569178..773d3390 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: record.ml 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: record.ml 13492 2010-10-04 21:20:01Z herbelin $ *) open Pp open Util @@ -259,8 +259,7 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls mind_entry_record = true; mind_entry_finite = recursivity_flag_of_kind finite; mind_entry_inds = [mie_ind] } in -(* TODO : maybe switch to KernelVerbose *) - let kn = Command.declare_mutual_inductive_with_eliminations KernelSilent mie [(paramimpls,[])] in + let kn = Command.declare_mutual_inductive_with_eliminations KernelVerbose mie [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) let cstr = (rsp,1) in let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in @@ -325,8 +324,8 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls (DefinitionEntry proj_entry, IsDefinition Definition) in let cref = ConstRef cst in - Impargs.declare_manual_implicits false cref paramimpls; - Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls); + Impargs.declare_manual_implicits false cref [paramimpls]; + Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls]; Classes.set_typeclass_transparency (EvalConstRef cst) false; if infer then Evd.fold (fun ev evi _ -> Recordops.declare_method (ConstRef cst) ev sign) sign (); cref, [proj_name, Some proj_cst] diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 7f8bcb9e..a00efc5c 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: vernac.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: vernac.ml 13488 2010-10-03 22:27:05Z herbelin $ *) (* Parsing of vernacular. *) @@ -44,7 +44,7 @@ let raise_with_file file exc = ((b, f, loc), e) | Stdpp.Exc_located (loc, e) when loc <> dummy_loc -> ((false,file, loc), e) - | _ -> ((false,file,cmdloc), re) + | Stdpp.Exc_located (_, e) | e -> ((false,file,cmdloc), e) in raise (Error_in_file (file, inner, disable_drop inex)) @@ -198,7 +198,10 @@ let rec vernac_com interpfun (loc,com) = with e -> stop(); raise e end - | v -> if not !just_parsing then interpfun v + | v -> + if not !just_parsing then + States.with_heavy_rollback interpfun + Cerrors.process_vernac_interp_error v in try @@ -239,7 +242,7 @@ and read_vernac_file verbosely s = * backtracking. *) let raw_do_vernac po = - vernac (States.with_heavy_rollback Vernacentries.interp) (po,None); + vernac Vernacentries.interp (po,None); Lib.add_frozen_state(); Lib.mark_end_of_command() diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 254f690c..d74711c2 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacentries.ml 13329 2010-07-26 11:05:39Z herbelin $ i*) +(*i $Id: vernacentries.ml 13492 2010-10-04 21:20:01Z herbelin $ i*) (* Concrete syntax of the mathematical vernacular MV V2.6 *) @@ -172,7 +172,7 @@ let show_match id = | [] -> assert false | [x] -> "| "^ x ^ " => \n" ^ acc | x::l -> - "| (" ^ List.fold_left (fun acc s -> acc ^ " " ^ s) x l ^ ")" + "| " ^ List.fold_left (fun acc s -> acc ^ " " ^ s) x l ^ " => \n" ^ acc) "end" patterns in msg (str ("match # with\n" ^ cases)) @@ -775,11 +775,11 @@ let vernac_syntactic_definition lid = Metasyntax.add_syntactic_definition (snd lid) let vernac_declare_implicits local r = function - | Some imps -> - Impargs.declare_manual_implicits local (smart_global r) ~enriching:false - (List.map (fun (ex,b,f) -> ex, (b,true,f)) imps) - | None -> + | [] -> Impargs.declare_implicits local (smart_global r) + | _::_ as imps -> + Impargs.declare_manual_implicits local (smart_global r) ~enriching:false + (List.map (List.map (fun (ex,b,f) -> ex, (b,true,f))) imps) let vernac_reserve bl = let sb_decl = (fun (idl,c) -> @@ -1113,7 +1113,7 @@ let vernac_print = function pp (Notation.pr_scope (Constrextern.without_symbols pr_lrawconstr) s) | PrintVisibility s -> pp (Notation.pr_visibility (Constrextern.without_symbols pr_lrawconstr) s) - | PrintAbout qid -> msgnl (print_about qid) + | PrintAbout qid -> msg (print_about qid) | PrintImplicit qid -> msg (print_impargs qid) (*spiwack: prints all the axioms and section variables used by a term *) | PrintAssumptions (o,r) -> diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 5eb220cb..b5af665c 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacexpr.ml 13332 2010-07-26 22:12:43Z msozeau $ i*) +(*i $Id: vernacexpr.ml 13492 2010-10-04 21:20:01Z herbelin $ i*) open Util open Names @@ -313,7 +313,7 @@ type vernac_expr = | VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) * locality_flag * onlyparsing_flag | VernacDeclareImplicits of locality_flag * reference or_by_notation * - (explicitation * bool * bool) list option + (explicitation * bool * bool) list list | VernacReserve of simple_binder list | VernacGeneralizable of locality_flag * (lident list) option | VernacSetOpacity of |