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 | |
| 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
| -rw-r--r-- | pretyping/evarconv.ml | 4 | ||||
| -rwxr-xr-x | pretyping/recordops.ml | 2 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 5f6f1522f..4af5a43cf 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -113,8 +113,8 @@ let apprec_nohdbeta env isevars c = let check_conv_record (t1,l1) (t2,l2) = try - let proji = reference_of_constr t1 in - let cstr = reference_of_constr t2 in + let proji = global_of_constr t1 in + let cstr = global_of_constr t2 in let { o_DEF = c; o_TABS = bs; o_TPARAMS = params; o_TCOMPS = us } = lookup_canonical_conversion (proji, cstr) in let params1, c1, extra_args1 = 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 diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index ee854e951..654f34e27 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -870,7 +870,7 @@ let reduce_to_ref_gen allow_product env sigma ref t = (str"Not an induction object of atomic type") | _ -> try - if reference_of_constr c = ref + if global_of_constr c = ref then it_mkProd_or_LetIn t l else raise Not_found with Not_found -> |