diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-23 15:40:23 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-23 15:40:23 +0000 |
| commit | ea798f046bf172626bd229906946803b0dd9cd96 (patch) | |
| tree | 9ae0dc2efe23bb660ebdc4f6cba33d8b94ca81a7 | |
| parent | c328c3f07818a382c68244f2de9627d9066b8f13 (diff) | |
Affichage opaque
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5133 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/tacred.ml | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 684dec0d3..e2bd273c4 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -739,15 +739,17 @@ let rec substlin env name n ol c = | (Rel _|Meta _|Var _|Sort _ |Evar _|Const _|Ind _|Construct _) -> (n,ol,c) -let string_of_evaluable_ref = function +let string_of_evaluable_ref env = function | EvalVarRef id -> string_of_id id - | EvalConstRef kn -> string_of_kn kn + | EvalConstRef kn -> + string_of_qualid + (Nametab.shortest_qualid_of_global (vars_of_env env) (ConstRef kn)) let unfold env sigma name = if is_evaluable env name then clos_norm_flags (unfold_red name) env sigma else - error (string_of_evaluable_ref name^" is opaque") + error (string_of_evaluable_ref env name^" is opaque") (* [unfoldoccs : (readable_constraints -> (int list * section_path) -> constr -> constr)] * Unfolds the constant name in a term c following a list of occurrences occl. @@ -759,9 +761,10 @@ let unfoldoccs env sigma (occl,name) c = | l -> match substlin env name 1 (Sort.list (<) l) c with | (_,[],uc) -> nf_betaiota uc - | (1,_,_) -> error ((string_of_evaluable_ref name)^" does not occur") + | (1,_,_) -> + error ((string_of_evaluable_ref env name)^" does not occur") | _ -> error ("bad occurrence numbers of " - ^(string_of_evaluable_ref name)) + ^(string_of_evaluable_ref env name)) (* Unfold reduction tactic: *) let unfoldn loccname env sigma c = |