diff options
| author | herbelin | 2001-10-17 12:49:19 +0000 |
|---|---|---|
| committer | herbelin | 2001-10-17 12:49:19 +0000 |
| commit | a6d858b84132bcb27bcc771f06a854cc94eef716 (patch) | |
| tree | df016a77a6d8d2f2a43fa9c2c01adc09b3be7c1b /proofs | |
| parent | 000ece141dc22e35365ea81558e8b6b1e65bd54c (diff) | |
Abstraction de l'immplementation de dirpath et implementation dans l'autre sens pour plus de partage entre chemins
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2126 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 0013fc32f4..8d44d146ee 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -104,7 +104,7 @@ let make_ids ast = function (* Gives Qualid's and makes the possible injection identifier -> qualid *) let make_qid = function | VArg (Qualid _) as arg -> arg - | VArg (Identifier id) -> VArg (Qualid (make_qualid [] id)) + | VArg (Identifier id) -> VArg (Qualid (make_short_qualid id)) | VArg (Constr c) -> (match (kind_of_term c) with | IsConst cst -> VArg (Qualid (qualid_of_sp cst)) @@ -122,7 +122,7 @@ let constr_of_id id = function if mem_named_context id hyps then mkVar id else - let csr = global_qualified_reference (make_qualid [] id) in + let csr = global_qualified_reference (make_short_qualid id) in (match kind_of_term csr with | IsVar _ -> raise Not_found | _ -> csr) @@ -209,7 +209,7 @@ let glob_const_nvar loc env qid = try (* We first look for a variable of the current proof *) match Nametab.repr_qualid qid with - | [],id -> + | d,id when is_empty_dirpath d -> (* lookup_value may raise Not_found *) (match Environ.lookup_named_value id env with | Some _ -> |