diff options
| author | herbelin | 2000-10-01 13:20:02 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-01 13:20:02 +0000 |
| commit | 9e6e6202c073fed0e2fc915d7f7e6ce927d55218 (patch) | |
| tree | ed17038b7fc77a5cba80c41616d4d18d66dd51f1 /pretyping | |
| parent | afdb9b7fa4a6ce1165b270ffdae4574897aa7c40 (diff) | |
Disparition du type oper mais nouveau type global_reference
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@620 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/class.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/class.ml b/pretyping/class.ml index 21935be3c7..f9c36315b6 100644 --- a/pretyping/class.ml +++ b/pretyping/class.ml @@ -443,9 +443,9 @@ let process_coercion sec_sp (((coe,coeinfo),s,t) as x) = if defined_in_sec sp sec_sp then let ((_,spid,spk)) = repr_path sp in let newsp = Lib.make_path spid CCI in - let id = Global.id_of_global (MutConstruct((newsp,i),j)) in + let id = Global.id_of_global (ConstructRef ((newsp,i),j)) in (((NAM_Constructor ((newsp,i),j)),coeinfo),s1,t1),id,p else ((coe,coeinfo),s1,t1), - Global.id_of_global (MutConstruct((sp,i),j)), + Global.id_of_global (ConstructRef ((sp,i),j)), p |