diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-05-20 15:42:55 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-05-20 15:42:55 +0000 |
| commit | 356506aee8f3b618487fc663f17ca32847f50db8 (patch) | |
| tree | 8819c95de665dbe88d87329a360726d902e55a1f /pretyping/recordops.ml | |
| parent | fc3eea4f6ab224df79d1c9e4350d96b639a0f923 (diff) | |
Adoption du nom canonique global_of_constr pour éviter confusion avec type reference
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7048 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/recordops.ml')
| -rwxr-xr-x | pretyping/recordops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 7f557d9b3..4157b383c 100755 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -144,7 +144,7 @@ let compute_canonical_projections (con,ind) = match spopt with | Some proji_sp -> let c, args = decompose_app t in - (try (ConstRef proji_sp, reference_of_constr c, args) :: l + (try (ConstRef proji_sp, global_of_constr c, args) :: l with Not_found -> l) | _ -> l) [] lps in |