diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-11-26 08:45:39 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-11-26 08:45:39 +0000 |
| commit | 53997574f2f411b7c4f28e4e6bf102eae82903fc (patch) | |
| tree | 4a62b4c0261eee619e7fd043a149c9e00cce0baa | |
| parent | ede38b4961bba30017d721050daec62c4ec0c906 (diff) | |
Evd vient apres Environ -> id_of_existential expanse
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@147 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | .depend | 14 | ||||
| -rw-r--r-- | kernel/environ.ml | 2 | ||||
| -rw-r--r-- | library/global.ml | 2 |
3 files changed, 10 insertions, 8 deletions
@@ -275,12 +275,14 @@ library/declare.cmx: kernel/constant.cmx kernel/evd.cmx kernel/generic.cmx \ kernel/inductive.cmx library/lib.cmx library/libobject.cmx \ kernel/names.cmx library/nametab.cmx kernel/reduction.cmx kernel/sign.cmx \ kernel/term.cmx kernel/univ.cmx lib/util.cmx library/declare.cmi -library/global.cmo: kernel/generic.cmi kernel/inductive.cmi \ - kernel/instantiate.cmi kernel/sign.cmi library/summary.cmi \ - kernel/term.cmi kernel/typing.cmi lib/util.cmi library/global.cmi -library/global.cmx: kernel/generic.cmx kernel/inductive.cmx \ - kernel/instantiate.cmx kernel/sign.cmx library/summary.cmx \ - kernel/term.cmx kernel/typing.cmx lib/util.cmx library/global.cmi +library/global.cmo: kernel/environ.cmi kernel/generic.cmi \ + kernel/inductive.cmi kernel/instantiate.cmi kernel/sign.cmi \ + library/summary.cmi kernel/term.cmi kernel/typing.cmi lib/util.cmi \ + library/global.cmi +library/global.cmx: kernel/environ.cmx kernel/generic.cmx \ + kernel/inductive.cmx kernel/instantiate.cmx kernel/sign.cmx \ + library/summary.cmx kernel/term.cmx kernel/typing.cmx lib/util.cmx \ + library/global.cmi library/impargs.cmo: kernel/constant.cmi kernel/evd.cmi kernel/generic.cmi \ library/global.cmi kernel/inductive.cmi kernel/names.cmi \ kernel/reduction.cmi library/summary.cmi kernel/term.cmi \ diff --git a/kernel/environ.ml b/kernel/environ.ml index b4aaed5f0..ccf3e1e20 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -131,7 +131,7 @@ let id_of_global env = function | Const sp -> basename sp | Evar ev -> - id_of_existential ev + id_of_string ("?" ^ string_of_int ev) | MutInd (sp,tyi) -> (* Does not work with extracted inductive types when the first inductive is logic : if tyi=0 then basename sp else *) diff --git a/library/global.ml b/library/global.ml index 3525d3834..9238b6e85 100644 --- a/library/global.ml +++ b/library/global.ml @@ -47,7 +47,7 @@ let import cenv = global_env := import cenv !global_env (* Some instanciations of functions from [Environ]. *) -let id_of_global = id_of_global !global_env +let id_of_global = Environ.id_of_global (unsafe_env_of_env !global_env) (* Re-exported functions of [Inductive], composed with [lookup_mind_specif]. *) |