diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-19 16:59:22 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-19 16:59:22 +0000 |
| commit | e7c4b9b422eda2c8b1b26fc46ecbdca3f137a4e1 (patch) | |
| tree | 1f183bc5f6dc239b34e2475e5fb0f86f79adde92 | |
| parent | 1a27e5f3ae317477f24893178023b714dbe4cc71 (diff) | |
Protection contre les warnings 'unused variable' de ocaml 3.09
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9503 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/vnorm.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 0b0c6ad73..46d67406a 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -54,10 +54,9 @@ let type_constructor mind mib typ params = let construct_of_constr const env tag typ = let (mind,_ as ind), allargs = find_rectype_a env typ in - let mib,mip as mind_s = lookup_mind_specif env ind in + let mib,mip = lookup_mind_specif env ind in let nparams = mib.mind_nparams in let i = invert_tag const tag mip.mind_reloc_tbl in - let c = (ind,i) in let params = Array.sub allargs 0 nparams in let ctyp = type_constructor mind mib (mip.mind_nf_lc.(i-1)) params in (mkApp(mkConstruct(ind,i), params), ctyp) |