diff options
| -rw-r--r-- | parsing/g_basevernac.ml4 | 2 | ||||
| -rw-r--r-- | parsing/pretty.ml | 8 | ||||
| -rwxr-xr-x | tools/coqdep_lexer.mll | 5 | ||||
| -rw-r--r-- | toplevel/errors.ml | 10 | ||||
| -rw-r--r-- | toplevel/usage.ml | 11 |
5 files changed, 22 insertions, 14 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 4abce12f3..1f4767704 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -138,7 +138,7 @@ GEXTEND Gram | IDENT "DelPath"; dir = stringarg -> <:ast< (DELPATH $dir) >> | IDENT "Print"; IDENT "Modules" -> <:ast< (PrintModules) >> - | IDENT "Print"; "Proof"; id = identarg -> + | IDENT "Print"; "Proof"; id = qualidarg -> <:ast< (PrintOpaqueId $id) >> (* Pris en compte dans PrintOption ci-dessous (CADUC) *) | IDENT "Print"; id = qualidarg -> <:ast< (PrintId $id) >> diff --git a/parsing/pretty.ml b/parsing/pretty.ml index ff17c3b74..6044767c2 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -446,10 +446,9 @@ let print_opaque_name qid = | IsConst (sp,_ as cst) -> let cb = Global.lookup_constant sp in if is_defined cb then - let typ = constant_type env Evd.empty cst in - print_typed_value (constant_value env cst, typ) + print_constant true " = " sp else - anomaly "print_opaque_name" + error "not a defined constant" | IsMutInd ((sp,_),_) -> print_mutual sp | IsMutConstruct cstr -> @@ -458,7 +457,8 @@ let print_opaque_name qid = | IsVar id -> let (c,ty) = lookup_named id env in print_named_decl (id,c,ty) - | _ -> failwith "print_name" + | _ -> + assert false with Not_found -> errorlabstrm "print_opaque" [< pr_qualid qid; 'sPC; 'sTR "not declared" >] diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index 9c4c482fb..29e4b04a3 100755 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -5,10 +5,11 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) + +(*i $Id$ i*) + { - (* $Id: *) - open Lexing type mL_token = Use_module of string diff --git a/toplevel/errors.ml b/toplevel/errors.ml index 3d1cbf1ae..3c18bf619 100644 --- a/toplevel/errors.ml +++ b/toplevel/errors.ml @@ -47,7 +47,7 @@ let rec explain_exn_default = function | Stack_overflow -> hOV 0 [< 'sTR "Stack overflow" >] | Ast.No_match s -> - hOV 0 [< 'sTR "Anomaly: Ast matching error: "; 'sTR s >] + hOV 0 [< 'sTR "Anomaly: Ast matching error: "; 'sTR s; report () >] | Anomaly (s,pps) -> hOV 1 [< 'sTR "Anomaly: "; where s; pps; report () >] | Match_failure(filename,pos1,pos2) -> @@ -98,6 +98,14 @@ let rec explain_exn_default = function hOV 0 [< 'sTR "Syntax error: Undefined token." >] | Lexer.Error (Bad_token s) -> hOV 0 [< 'sTR "Syntax error: Bad token"; 'sPC; 'sTR s; 'sTR "." >] + | Assert_failure (s,b,e) -> + hOV 0 [< 'sTR "Anomaly: assert failure"; 'sPC; + if s <> "" then + [< 'sTR ("(file \"" ^ s ^ "\", characters "); + 'iNT b; 'sTR "-"; 'iNT e; 'sTR ")" >] + else + [< >]; + report () >] | reraise -> hOV 0 [< 'sTR "Anomaly: Uncaught exception "; 'sTR (Printexc.to_string reraise); report () >] diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 68f4a0bc2..8dc848d3c 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -18,7 +18,7 @@ let version () = let print_usage_channel co command = output_string co command; - output_string co "Options are:\n"; + output_string co "Coq options are:\n"; output_string co " -I dir add directory dir in the include path -include dir (idem) @@ -37,7 +37,6 @@ let print_usage_channel co command = -require f load Coq object file f.vo and import it (Require f.) -opt run the native-code version of Coq or Coq_SearchIsos - -image f specify an alternative binary image f -bindir dir specify an alternative directory for the binaries -libdir dir specify an alternative directory for the library @@ -56,11 +55,11 @@ let print_usage_channel co command = let print_usage = print_usage_channel stderr let print_usage_coqtop () = - print_usage "Usage: coqtop <options>\n"; - output_string stderr -" -searchisos run Coq_SearchIsos\n" + print_usage "Usage: coqtop <options>\n\n" let print_usage_coqc () = - print_usage "Usage: coqc [-t] [-verbose] <options> file...\n + print_usage "Usage: coqc <options> <Coq options> file...\n +options are: -verbose compile verbosely + -image f specify an alternative executable for Coq -t keep temporary files\n\n" |