diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-16 15:58:48 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-16 15:58:48 +0000 |
| commit | 3c248785237d8dea037da274f4acc0229894de93 (patch) | |
| tree | 4501aca5e725d5f62ffd9f959a8956f30bf432eb /proofs | |
| parent | 649e7e98e0067a7ae2a3990b9629dcec66b47497 (diff) | |
ident au lieu de string pour le nom de base de qualid
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1395 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacinterp.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index c98840d73..9f68b896f 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -186,12 +186,12 @@ let glob_const_nvar loc env qid = try (* We first look for a variable of the current proof *) match repr_qualid qid with - | [],s -> - let id = id_of_string s in + | [],id -> (* lookup_value may raise Not_found *) (match Environ.lookup_named_value id env with | Some _ -> EvalVarRef id - | None -> error (s^" does not denote an evaluable constant")) + | None -> error ((string_of_id id)^ + " does not denote an evaluable constant")) | _ -> raise Not_found with Not_found -> try |