diff options
| author | filliatr | 2001-04-06 12:45:24 +0000 |
|---|---|---|
| committer | filliatr | 2001-04-06 12:45:24 +0000 |
| commit | 1d641d1c2fcd97b6fd60369de8b4a7e6a26b1051 (patch) | |
| tree | f61e6163b89eaa24e7541ff94989fe9e6da46bb7 /parsing | |
| parent | 763102437580da08cd96d06d05d99dc1a3eda1b1 (diff) | |
bug Print Proof; usage coqtop/coqc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1552 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_basevernac.ml4 | 2 | ||||
| -rw-r--r-- | parsing/pretty.ml | 8 |
2 files changed, 5 insertions, 5 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 4abce12f34..1f47677044 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 ff17c3b744..6044767c2c 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" >] |