diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 14 |
1 files changed, 7 insertions, 7 deletions
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) -> |